Regenerate the test files

1 files changed, 14 insertions, 14 deletions

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index d5a6e535..abec8e88 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -13,8 +13,8 @@ Module Demo.
 Definition choose
   (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
   if b
-  then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
-  else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+  then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+  else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
 .
 
 (** [demo::mul2_add1]:
@@ -79,16 +79,16 @@ Fixpoint list_nth_mut
     | CList_CCons x tl =>
       if i s= 0%u32
       then
-        let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
-        Return (x, back_'a)
+        let back := fun (ret : T) => Return (CList_CCons ret tl) in
+        Return (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut T n1 tl i1;
         let (t, list_nth_mut_back) := p in
-        let back_'a :=
+        let back :=
           fun (ret : T) =>
             tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in
-        Return (t, back_'a))
+        Return (t, back))
     | CList_CNil => Fail_ Failure
     end
   end
@@ -107,15 +107,15 @@ Fixpoint list_nth_mut1_loop
     | CList_CCons x tl =>
       if i s= 0%u32
       then
-        let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
-        Return (x, back_'a)
+        let back := fun (ret : T) => Return (CList_CCons ret tl) in
+        Return (x, back)
       else (
         i1 <- u32_sub i 1%u32;
         p <- list_nth_mut1_loop T n1 tl i1;
-        let (t, back_'a) := p in
-        let back_'a1 :=
-          fun (ret : T) => tl1 <- back_'a ret; Return (CList_CCons x tl1) in
-        Return (t, back_'a1))
+        let (t, back) := p in
+        let back1 :=
+          fun (ret : T) => tl1 <- back ret; Return (CList_CCons x tl1) in
+        Return (t, back1))
     | CList_CNil => Fail_ Failure
     end
   end
@@ -155,10 +155,10 @@ Fixpoint list_tail
     | CList_CCons t tl =>
       p <- list_tail T n1 tl;
       let (c, list_tail_back) := p in
-      let back_'a :=
+      let back :=
         fun (ret : CList_t T) =>
           tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in
-      Return (c, back_'a)
+      Return (c, back)
     | CList_CNil => Return (CList_CNil, Return)
     end
   end