Bump charon

4 files changed, 15 insertions, 15 deletions

diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 5ff17341..cd6a4b87 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -376,7 +376,7 @@ Definition non_copyable_array : result unit :=
 .
 
 (** [arrays::sum]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 245:0-253:1 *)
+    Source: 'tests/src/arrays.rs', lines 247:4-253:1 *)
 Fixpoint sum_loop
   (n : nat) (s : slice u32) (sum1 : u32) (i : usize) : result u32 :=
   match n with
@@ -400,7 +400,7 @@ Definition sum (n : nat) (s : slice u32) : result u32 :=
 .
 
 (** [arrays::sum2]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 255:0-264:1 *)
+    Source: 'tests/src/arrays.rs', lines 258:4-264:1 *)
 Fixpoint sum2_loop
   (n : nat) (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) :
   result u32
@@ -508,7 +508,7 @@ Definition ite : result unit :=
 .
 
 (** [arrays::zero_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 306:0-313:1 *)
+    Source: 'tests/src/arrays.rs', lines 308:4-313:1 *)
 Fixpoint zero_slice_loop
   (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) :=
   match n with
@@ -532,7 +532,7 @@ Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
 .
 
 (** [arrays::iter_mut_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 315:0-321:1 *)
+    Source: 'tests/src/arrays.rs', lines 317:4-321:1 *)
 Fixpoint iter_mut_slice_loop
   (n : nat) (len : usize) (i : usize) : result unit :=
   match n with
@@ -551,7 +551,7 @@ Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
 .
 
 (** [arrays::sum_mut_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 323:0-331:1 *)
+    Source: 'tests/src/arrays.rs', lines 325:4-331:1 *)
 Fixpoint sum_mut_slice_loop
   (n : nat) (a : slice u32) (i : usize) (s : u32) : result u32 :=
   match n with
diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v
index 1c6092ba..bb9fe90e 100644
--- a/tests/coq/betree/Betree_Funs.v
+++ b/tests/coq/betree/Betree_Funs.v
@@ -89,7 +89,7 @@ Definition betree_upsert_update
 .
 
 (** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
-    Source: 'src/betree.rs', lines 276:4-284:5 *)
+    Source: 'src/betree.rs', lines 278:8-284:5 *)
 Fixpoint betree_List_len_loop
   (T : Type) (n : nat) (self : betree_List_t T) (len : u64) : result u64 :=
   match n with
@@ -111,7 +111,7 @@ Definition betree_List_len
 .
 
 (** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
-    Source: 'src/betree.rs', lines 304:4-312:5 *)
+    Source: 'src/betree.rs', lines 305:8-312:5 *)
 Fixpoint betree_List_reverse_loop
   (T : Type) (n : nat) (self : betree_List_t T) (out : betree_List_t T) :
   result (betree_List_t T)
@@ -135,7 +135,7 @@ Definition betree_List_reverse
 .
 
 (** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
-    Source: 'src/betree.rs', lines 287:4-302:5 *)
+    Source: 'src/betree.rs', lines 289:8-302:5 *)
 Fixpoint betree_List_split_at_loop
   (T : Type) (n : nat) (n1 : u64) (beg : betree_List_t T)
   (self : betree_List_t T) :
@@ -204,7 +204,7 @@ Definition betree_ListPairU64T_head_has_key
 .
 
 (** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
-    Source: 'src/betree.rs', lines 355:4-370:5 *)
+    Source: 'src/betree.rs', lines 358:8-370:5 *)
 Fixpoint betree_ListPairU64T_partition_at_pivot_loop
   (T : Type) (n : nat) (pivot : u64) (beg : betree_List_t (u64 * T))
   (end1 : betree_List_t (u64 * T)) (self : betree_List_t (u64 * T)) :
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index d63c6f72..39bd5098 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -70,7 +70,7 @@ Definition hashMap_new (T : Type) (n : nat) : result (HashMap_t T) :=
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 91:4-99:5 *)
+    Source: 'tests/src/hashmap.rs', lines 94:8-99:5 *)
 Fixpoint hashMap_clear_loop
   (T : Type) (n : nat) (slots : alloc_vec_Vec (AList_t T)) (i : usize) :
   result (alloc_vec_Vec (AList_t T))
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 87b05193..a29394e1 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
 Module Loops.
 
 (** [loops::sum]: loop 0:
-    Source: 'tests/src/loops.rs', lines 8:0-18:1 *)
+    Source: 'tests/src/loops.rs', lines 10:4-18:1 *)
 Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -27,7 +27,7 @@ Definition sum (n : nat) (max : u32) : result u32 :=
 .
 
 (** [loops::sum_with_mut_borrows]: loop 0:
-    Source: 'tests/src/loops.rs', lines 23:0-35:1 *)
+    Source: 'tests/src/loops.rs', lines 25:4-35:1 *)
 Fixpoint sum_with_mut_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
@@ -49,7 +49,7 @@ Definition sum_with_mut_borrows (n : nat) (max : u32) : result u32 :=
 .
 
 (** [loops::sum_with_shared_borrows]: loop 0:
-    Source: 'tests/src/loops.rs', lines 38:0-52:1 *)
+    Source: 'tests/src/loops.rs', lines 40:4-52:1 *)
 Fixpoint sum_with_shared_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
@@ -71,7 +71,7 @@ Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 :=
 .
 
 (** [loops::sum_array]: loop 0:
-    Source: 'tests/src/loops.rs', lines 54:0-62:1 *)
+    Source: 'tests/src/loops.rs', lines 56:4-62:1 *)
 Fixpoint sum_array_loop
   (N : usize) (n : nat) (a : array u32 N) (i : usize) (s : u32) : result u32 :=
   match n with
@@ -94,7 +94,7 @@ Definition sum_array (N : usize) (n : nat) (a : array u32 N) : result u32 :=
 .
 
 (** [loops::clear]: loop 0:
-    Source: 'tests/src/loops.rs', lines 66:0-72:1 *)
+    Source: 'tests/src/loops.rs', lines 67:4-72:1 *)
 Fixpoint clear_loop
   (n : nat) (v : alloc_vec_Vec u32) (i : usize) : result (alloc_vec_Vec u32) :=
   match n with