summaryrefslogtreecommitdiff
path: root/tests/coq/demo
diff options
context:
space:
mode:
authorSon Ho2024-03-20 06:17:41 +0100
committerSon Ho2024-03-20 06:17:41 +0100
commit5e99d127e0a746f5779779756fccf79f15c19d10 (patch)
tree6d10d613179568346e19cbc6bf95c6dd6897f574 /tests/coq/demo
parente6f002cfc1dfa41362bbb3a005c4261d09c52c58 (diff)
Regenerate the code
Diffstat (limited to '')
-rw-r--r--tests/coq/demo/Demo.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 2fccf6c0..d5a6e535 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -37,7 +37,7 @@ Definition incr (x : u32) : result u32 :=
(** [demo::use_incr]:
Source: 'src/demo.rs', lines 25:0-25:17 *)
Definition use_incr : result unit :=
- i <- incr 0%u32; i1 <- incr i; _ <- incr i1; Return tt
+ x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt
.
(** [demo::CList]