Merge pull request #111 from AeneasVerif/son/names

Improve the names used for the variables in the generated code

1 files changed, 5 insertions, 6 deletions

diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index ddc5e7a8..c2f47ad1 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -23,8 +23,8 @@ let _ = assert_norm (test_incr = Return ())
 let choose
   (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
   if b
-  then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
-  else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+  then let back = fun ret -> Return (ret, y) in Return (x, back)
+  else let back = fun ret -> Return (x, ret) in Return (y, back)
 
 (** [paper::test_choose]:
     Source: 'src/paper.rs', lines 23:0-23:20 *)
@@ -57,15 +57,14 @@ let rec list_nth_mut
   begin match l with
   | List_Cons x tl ->
     if i = 0
-    then
-      let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
+    then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
     else
       let* i1 = u32_sub i 1 in
       let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
-      let back_'a =
+      let back =
         fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
         in
-      Return (x1, back_'a)
+      Return (x1, back)
   | List_Nil -> Fail Failure
   end