Merge pull request #111 from AeneasVerif/son/names

Improve the names used for the variables in the generated code

1 files changed, 39 insertions, 39 deletions

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 7c83a014..ae529cf8 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -375,18 +375,18 @@ Fixpoint list_nth_mut_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
-          let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back_'a, back_'b)
+          let back'a := fun (ret : T) => Return (List_Cons ret tl0) in
+          let back'b := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back'a, back'b)
         else (
           i1 <- u32_sub i 1%u32;
           t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
-          let '(p, back_'a, back_'b) := t in
-          let back_'a1 :=
-            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
-          let back_'b1 :=
-            fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
-          Return (p, back_'a1, back_'b1))
+          let '(p, back'a, back'b) := t in
+          let back'a1 :=
+            fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in
+          let back'b1 :=
+            fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in
+          Return (p, back'a1, back'b1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -451,21 +451,21 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a :=
+          let back :=
             fun (ret : (T * T)) =>
               let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1)
             in
-          Return ((x0, x1), back_'a)
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
-          let (p1, back_'a) := p in
-          let back_'a1 :=
+          let (p1, back) := p in
+          let back1 :=
             fun (ret : (T * T)) =>
-              p2 <- back_'a ret;
+              p2 <- back ret;
               let (tl01, tl11) := p2 in
               Return (List_Cons x0 tl01, List_Cons x1 tl11) in
-          Return (p1, back_'a1))
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -531,15 +531,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
-          Return ((x0, x1), back_'a)
+          let back := fun (ret : T) => Return (List_Cons ret tl0) in
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1;
-          let (p1, back_'a) := p in
-          let back_'a1 :=
-            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
-          Return (p1, back_'a1))
+          let (p1, back) := p in
+          let back1 :=
+            fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -571,15 +571,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
-          Return ((x0, x1), back_'a)
+          let back := fun (ret : T) => Return (List_Cons ret tl0) in
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1;
-          let (p1, back_'a) := p in
-          let back_'a1 :=
-            fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
-          Return (p1, back_'a1))
+          let (p1, back) := p in
+          let back1 :=
+            fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -611,15 +611,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back_'b)
+          let back := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1;
-          let (p1, back_'b) := p in
-          let back_'b1 :=
-            fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
-          Return (p1, back_'b1))
+          let (p1, back) := p in
+          let back1 :=
+            fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure
@@ -651,15 +651,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
       | List_Cons x1 tl1 =>
         if i s= 0%u32
         then
-          let back_'a := fun (ret : T) => Return (List_Cons ret tl1) in
-          Return ((x0, x1), back_'a)
+          let back := fun (ret : T) => Return (List_Cons ret tl1) in
+          Return ((x0, x1), back)
         else (
           i1 <- u32_sub i 1%u32;
           p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
-          let (p1, back_'a) := p in
-          let back_'a1 :=
-            fun (ret : T) => tl11 <- back_'a ret; Return (List_Cons x1 tl11) in
-          Return (p1, back_'a1))
+          let (p1, back) := p in
+          let back1 :=
+            fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
+          Return (p1, back1))
       | List_Nil => Fail_ Failure
       end
     | List_Nil => Fail_ Failure