diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/demo/Demo.v | 2 |
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] |