summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq')
-rw-r--r--tests/coq/arrays/Arrays.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 371e4a12..6e4ab188 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -289,9 +289,9 @@ Definition index_all : result u32 :=
let (s1, to_slice_mut_back) := p in
p1 <- index_mut_slice_u32_0 s1;
let (i7, s2) := p1 in
- i8 <- u32_add i6 i7;
+ i9 <- u32_add i6 i7;
_ <- to_slice_mut_back s2;
- Ok i8
+ Ok i9
.
(** [arrays::update_array]: