diff options
author | Guillaume Boisseau | 2024-06-18 13:49:43 +0200 |
---|---|---|
committer | GitHub | 2024-06-18 13:49:43 +0200 |
commit | 370f2668f0a36fb31ed9abb4ba613dad333cf406 (patch) | |
tree | d1a6549cdd2f8e20366b8a5feaa1550fc10fe783 /tests/coq/misc | |
parent | 43a9fb0fa5a1c03a7cce575a052f0d4201189d1d (diff) | |
parent | 926eb538cc35cf9a818a6905ff4ce58eeb3db9c4 (diff) |
Merge pull request #251 from Nadrieril/bump-charon2
Diffstat (limited to 'tests/coq/misc')
-rw-r--r-- | tests/coq/misc/Loops.v | 10 |
1 files changed, 5 insertions, 5 deletions
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 |