From e288482f437a5f259be5f81eb996b5b28158b300 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:51:03 +0200
Subject: Update output files

---
 tests/coq/demo/Demo.v | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'tests/coq/demo')

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 1cccbeda..e8c3a694 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
 Module Demo.
 
 (** [demo::choose]:
-    Source: 'tests/src/demo.rs', lines 6:0-6:70 *)
+    Source: 'tests/src/demo.rs', lines 7:0-7:70 *)
 Definition choose
   (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
   if b
@@ -18,30 +18,30 @@ Definition choose
 .
 
 (** [demo::mul2_add1]:
-    Source: 'tests/src/demo.rs', lines 14:0-14:31 *)
+    Source: 'tests/src/demo.rs', lines 15:0-15:31 *)
 Definition mul2_add1 (x : u32) : result u32 :=
   i <- u32_add x x; u32_add i 1%u32
 .
 
 (** [demo::use_mul2_add1]:
-    Source: 'tests/src/demo.rs', lines 18:0-18:43 *)
+    Source: 'tests/src/demo.rs', lines 19:0-19:43 *)
 Definition use_mul2_add1 (x : u32) (y : u32) : result u32 :=
   i <- mul2_add1 x; u32_add i y
 .
 
 (** [demo::incr]:
-    Source: 'tests/src/demo.rs', lines 22:0-22:31 *)
+    Source: 'tests/src/demo.rs', lines 23:0-23:31 *)
 Definition incr (x : u32) : result u32 :=
   u32_add x 1%u32.
 
 (** [demo::use_incr]:
-    Source: 'tests/src/demo.rs', lines 26:0-26:17 *)
+    Source: 'tests/src/demo.rs', lines 27:0-27:17 *)
 Definition use_incr : result unit :=
   x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Ok tt
 .
 
 (** [demo::CList]
-    Source: 'tests/src/demo.rs', lines 35:0-35:17 *)
+    Source: 'tests/src/demo.rs', lines 36:0-36:17 *)
 Inductive CList_t (T : Type) :=
 | CList_CCons : T -> CList_t T -> CList_t T
 | CList_CNil : CList_t T
@@ -51,7 +51,7 @@ Arguments CList_CCons { _ }.
 Arguments CList_CNil { _ }.
 
 (** [demo::list_nth]:
-    Source: 'tests/src/demo.rs', lines 40:0-40:56 *)
+    Source: 'tests/src/demo.rs', lines 41:0-41:56 *)
 Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
   match n with
   | O => Fail_ OutOfFuel
@@ -65,7 +65,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
 .
 
 (** [demo::list_nth_mut]:
-    Source: 'tests/src/demo.rs', lines 55:0-55:68 *)
+    Source: 'tests/src/demo.rs', lines 56:0-56:68 *)
 Fixpoint list_nth_mut
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -91,7 +91,7 @@ Fixpoint list_nth_mut
 .
 
 (** [demo::list_nth_mut1]: loop 0:
-    Source: 'tests/src/demo.rs', lines 70:0-79:1 *)
+    Source: 'tests/src/demo.rs', lines 71:0-80:1 *)
 Fixpoint list_nth_mut1_loop
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -116,7 +116,7 @@ Fixpoint list_nth_mut1_loop
 .
 
 (** [demo::list_nth_mut1]:
-    Source: 'tests/src/demo.rs', lines 70:0-70:77 *)
+    Source: 'tests/src/demo.rs', lines 71:0-71:77 *)
 Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -125,7 +125,7 @@ Definition list_nth_mut1
 .
 
 (** [demo::i32_id]:
-    Source: 'tests/src/demo.rs', lines 81:0-81:28 *)
+    Source: 'tests/src/demo.rs', lines 82:0-82:28 *)
 Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -137,7 +137,7 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
 .
 
 (** [demo::list_tail]:
-    Source: 'tests/src/demo.rs', lines 89:0-89:64 *)
+    Source: 'tests/src/demo.rs', lines 90:0-90:64 *)
 Fixpoint list_tail
   (T : Type) (n : nat) (l : CList_t T) :
   result ((CList_t T) * (CList_t T -> result (CList_t T)))
@@ -159,7 +159,7 @@ Fixpoint list_tail
 .
 
 (** Trait declaration: [demo::Counter]
-    Source: 'tests/src/demo.rs', lines 98:0-98:17 *)
+    Source: 'tests/src/demo.rs', lines 99:0-99:17 *)
 Record Counter_t (Self : Type) := mkCounter_t {
   Counter_t_incr : Self -> result (usize * Self);
 }.
@@ -168,19 +168,19 @@ Arguments mkCounter_t { _ }.
 Arguments Counter_t_incr { _ }.
 
 (** [demo::{(demo::Counter for usize)}::incr]:
-    Source: 'tests/src/demo.rs', lines 103:4-103:31 *)
+    Source: 'tests/src/demo.rs', lines 104:4-104:31 *)
 Definition counterUsize_incr (self : usize) : result (usize * usize) :=
   self1 <- usize_add self 1%usize; Ok (self, self1)
 .
 
 (** Trait implementation: [demo::{(demo::Counter for usize)}]
-    Source: 'tests/src/demo.rs', lines 102:0-102:22 *)
+    Source: 'tests/src/demo.rs', lines 103:0-103:22 *)
 Definition CounterUsize : Counter_t usize := {|
   Counter_t_incr := counterUsize_incr;
 |}.
 
 (** [demo::use_counter]:
-    Source: 'tests/src/demo.rs', lines 110:0-110:59 *)
+    Source: 'tests/src/demo.rs', lines 111:0-111:59 *)
 Definition use_counter
   (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) :=
   counterInst.(Counter_t_incr) cnt
-- 
cgit v1.2.3