From 5209b9976107592802327bac30e8b98fbb9c2d2f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2024 13:37:38 +0200
Subject: Update charon

---
 tests/coq/betree/BetreeMain_Funs.v                   | 2 +-
 tests/fstar/betree/BetreeMain.Funs.fst               | 2 +-
 tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 2 +-
 tests/lean/Betree.lean                               | 1 +
 tests/lean/BetreeMain/Funs.lean                      | 2 +-
 5 files changed, 5 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/Betree.lean

(limited to 'tests')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index c31713be..e0a1d8a2 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -827,7 +827,7 @@ Definition betree_BeTree_lookup
 .
 
 (** [betree_main::main]:
-    Source: 'src/betree_main.rs', lines 5:0-5:9 *)
+    Source: 'src/main.rs', lines 4:0-4:9 *)
 Definition main : result unit :=
   Ok tt.
 
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 89396df0..9942ef68 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -667,7 +667,7 @@ let betree_BeTree_lookup
   Ok (st1, (o, { self with root = n }))
 
 (** [betree_main::main]:
-    Source: 'src/betree_main.rs', lines 5:0-5:9 *)
+    Source: 'src/main.rs', lines 4:0-4:9 *)
 let main : result unit =
   Ok ()
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 89396df0..9942ef68 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -667,7 +667,7 @@ let betree_BeTree_lookup
   Ok (st1, (o, { self with root = n }))
 
 (** [betree_main::main]:
-    Source: 'src/betree_main.rs', lines 5:0-5:9 *)
+    Source: 'src/main.rs', lines 4:0-4:9 *)
 let main : result unit =
   Ok ()
 
diff --git a/tests/lean/Betree.lean b/tests/lean/Betree.lean
new file mode 100644
index 00000000..58bee0c4
--- /dev/null
+++ b/tests/lean/Betree.lean
@@ -0,0 +1 @@
+import Betree.Funs
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index f0032d51..7cc52159 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -702,7 +702,7 @@ def betree.BeTree.lookup
   Result.ok (st1, (o, { self with root := n }))
 
 /- [betree_main::main]:
-   Source: 'src/betree_main.rs', lines 5:0-5:9 -/
+   Source: 'src/main.rs', lines 4:0-4:9 -/
 def main : Result Unit :=
   Result.ok ()
 
-- 
cgit v1.2.3