Merge pull request #111 from AeneasVerif/son/names

Improve the names used for the variables in the generated code

1 files changed, 6 insertions, 6 deletions

diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 76dc4cf6..d4035104 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -321,8 +321,8 @@ Check (test_split_list )%return.
 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)
 .
 
 (** [no_nested_borrows::choose_test]:
@@ -399,16 +399,16 @@ Fixpoint list_nth_mut
   | List_Cons x tl =>
     if i s= 0%u32
     then
-      let back_'a := fun (ret : T) => Return (List_Cons ret tl) in
-      Return (x, back_'a)
+      let back := fun (ret : T) => Return (List_Cons ret tl) in
+      Return (x, back)
     else (
       i1 <- u32_sub i 1%u32;
       p <- list_nth_mut T 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 (List_Cons x tl1)
         in
-      Return (t, back_'a))
+      Return (t, back))
   | List_Nil => Fail_ Failure
   end
 .