From a781ea75c1860c76c5577faa57efcdb0db910612 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 10:56:52 +0100
Subject: Added meta information to names_map_id field in names_map type

---
 compiler/ExtractBase.ml | 45 +++++++++++++++++++++++----------------------
 1 file changed, 23 insertions(+), 22 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..96f816cb 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -237,7 +237,7 @@ module IdSet = Collections.MakeSet (IdOrderedType)
   *)
 type names_map = {
   id_to_name : string IdMap.t;
-  name_to_id : id StringMap.t;
+  name_to_id : (id * Meta.meta option) StringMap.t;
       (** The name to id map is used to look for name clashes, and generate nice
           debugging messages: if there is a name clash, it is useful to know
           precisely which identifiers are mapped to the same name...
@@ -253,8 +253,8 @@ let empty_names_map : names_map =
   }
 
 (** Small helper to report name collision *)
-let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
-    (name : string) : unit =
+let report_name_collision (id_to_string : id -> string)
+    (id1, meta : id * Meta.meta option) (id2 : id) (name : string) : unit =
   let id1 = "\n- " ^ id_to_string id1 in
   let id2 = "\n- " ^ id_to_string id2 in
   let err =
@@ -263,9 +263,10 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
   (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ None err
+  save_error __FILE__ __LINE__ meta err
 
-let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
+let names_map_get_id_from_name (name : string) (nm : names_map) :
+    (id * Meta.meta option) option =
   StringMap.find_opt name nm.name_to_id
 
 let names_map_check_collision (id_to_string : id -> string) (id : id)
@@ -277,15 +278,15 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
       report_name_collision id_to_string clash id name
 
 (** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id : id) (name : string) (nm : names_map) :
+let names_map_add_unchecked (id, meta : id * Meta.meta option) (name : string) (nm : names_map) :
     names_map =
   (* Insert *)
   let id_to_name = IdMap.add id name nm.id_to_name in
-  let name_to_id = StringMap.add name id nm.name_to_id in
+  let name_to_id= StringMap.add name (id, meta) nm.name_to_id in
   let names_set = StringSet.add name nm.names_set in
   { id_to_name; name_to_id; names_set }
 
-let names_map_add (id_to_string : id -> string) (id : id) (name : string)
+let names_map_add (id_to_string : id -> string) (id, meta : id * meta option) (name : string)
     (nm : names_map) : names_map =
   (* Check if there is a clash *)
   names_map_check_collision id_to_string id name nm;
@@ -296,9 +297,9 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
        ^ ":\nThe chosen name is already in the names set: " ^ name
      in
      (* If we fail hard on errors, raise an exception *)
-     save_error __FILE__ __LINE__ None err);
+     save_error __FILE__ __LINE__ meta err);
   (* Insert *)
-  names_map_add_unchecked id name nm
+  names_map_add_unchecked (id, meta) name nm
 
 (** The unsafe names map stores mappings from identifiers to names which might
     collide. For some backends and some names, it might be acceptable to have
@@ -384,7 +385,7 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
+let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (name : string)
     (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
@@ -415,10 +416,10 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
     *)
     let strict_names_map =
       if strict_collisions id then
-        names_map_add id_to_string id name nm.strict_names_map
+        names_map_add id_to_string (id, meta) name nm.strict_names_map
       else nm.strict_names_map
     in
-    let names_map = names_map_add id_to_string id name nm.names_map in
+    let names_map = names_map_add id_to_string (id, meta) name nm.names_map in
     { nm with strict_names_map; names_map }
 
 (** The [id_to_string] function to print nice debugging messages if there are
@@ -468,20 +469,20 @@ type names_map_init = {
 
 let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (TypeId (TAssumed id)) name nm
+  names_maps_add None id_to_string (TypeId (TAssumed id)) name nm
 
 let names_maps_add_assumed_struct (id_to_string : id -> string)
     (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (StructId (TAssumed id)) name nm
+  names_maps_add None id_to_string (StructId (TAssumed id)) name nm
 
 let names_maps_add_assumed_variant (id_to_string : id -> string)
     (id : assumed_ty) (variant_id : VariantId.id) (name : string)
     (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm
+  names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
 
-let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
+let names_maps_add_function (id_to_string : id -> string) (fid, meta : fun_id * meta option)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (FunId fid) name nm
+  names_maps_add meta id_to_string (FunId fid) name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
 let char_name () = if !backend = Lean then "Char" else "char"
@@ -659,7 +660,7 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
 let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
-  let names_maps = names_maps_add id_to_string id name ctx.names_maps in
+  let names_maps = names_maps_add (Some meta) id_to_string id name ctx.names_maps in
   { ctx with names_maps }
 
 let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1125,7 +1126,7 @@ let initialize_names_maps () : names_maps =
         (* There is duplication in the keywords so we don't check the collisions
            while registering them (what is important is that there are no collisions
            between keywords and user-defined identifiers) *)
-        names_map_add_unchecked UnknownId name nm)
+        names_map_add_unchecked (UnknownId, None) name nm)
       strict_names_map keywords
   in
   let nm = { names_map; unsafe_names_map; strict_names_map } in
@@ -1155,9 +1156,9 @@ let initialize_names_maps () : names_maps =
   in
   let assumed_functions =
     List.map
-      (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name))
+      (fun (fid, name) -> ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
       init.assumed_llbc_functions
-    @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
+    @ List.map (fun (fid, name) -> ((Pure fid, None), name)) init.assumed_pure_functions
   in
   let nm =
     List.fold_left
-- 
cgit v1.2.3


From a25f3bc7fe1dcddc952b4dcbb7b732bdf095197e Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 18:23:46 +0200
Subject: rebased branch

---
 compiler/ExtractBase.ml | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 96f816cb..34b5ad64 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -254,7 +254,7 @@ let empty_names_map : names_map =
 
 (** Small helper to report name collision *)
 let report_name_collision (id_to_string : id -> string)
-    (id1, meta : id * Meta.meta option) (id2 : id) (name : string) : unit =
+    ((id1, meta) : id * Meta.meta option) (id2 : id) (name : string) : unit =
   let id1 = "\n- " ^ id_to_string id1 in
   let id2 = "\n- " ^ id_to_string id2 in
   let err =
@@ -278,16 +278,16 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
       report_name_collision id_to_string clash id name
 
 (** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id, meta : id * Meta.meta option) (name : string) (nm : names_map) :
-    names_map =
+let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
+    (nm : names_map) : names_map =
   (* Insert *)
   let id_to_name = IdMap.add id name nm.id_to_name in
-  let name_to_id= StringMap.add name (id, meta) nm.name_to_id in
+  let name_to_id = StringMap.add name (id, meta) nm.name_to_id in
   let names_set = StringSet.add name nm.names_set in
   { id_to_name; name_to_id; names_set }
 
-let names_map_add (id_to_string : id -> string) (id, meta : id * meta option) (name : string)
-    (nm : names_map) : names_map =
+let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
+    (name : string) (nm : names_map) : names_map =
   (* Check if there is a clash *)
   names_map_check_collision id_to_string id name nm;
   (* Sanity check *)
@@ -385,8 +385,8 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (name : string)
-    (nm : names_maps) : names_maps =
+let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
+    (id : id) (name : string) (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
      type information to disambiguate field projections.
@@ -480,8 +480,9 @@ let names_maps_add_assumed_variant (id_to_string : id -> string)
     (nm : names_maps) : names_maps =
   names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
 
-let names_maps_add_function (id_to_string : id -> string) (fid, meta : fun_id * meta option)
-    (name : string) (nm : names_maps) : names_maps =
+let names_maps_add_function (id_to_string : id -> string)
+    ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
+    names_maps =
   names_maps_add meta id_to_string (FunId fid) name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
@@ -660,7 +661,9 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
 let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
-  let names_maps = names_maps_add (Some meta) id_to_string id name ctx.names_maps in
+  let names_maps =
+    names_maps_add (Some meta) id_to_string id name ctx.names_maps
+  in
   { ctx with names_maps }
 
 let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1156,9 +1159,12 @@ let initialize_names_maps () : names_maps =
   in
   let assumed_functions =
     List.map
-      (fun (fid, name) -> ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
+      (fun (fid, name) ->
+        ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
       init.assumed_llbc_functions
-    @ List.map (fun (fid, name) -> ((Pure fid, None), name)) init.assumed_pure_functions
+    @ List.map
+        (fun (fid, name) -> ((Pure fid, None), name))
+        init.assumed_pure_functions
   in
   let nm =
     List.fold_left
-- 
cgit v1.2.3


From 8a8f3ee2e444542112a3b0ea0b4e6283b1893aaa Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 10:57:01 +0200
Subject: Make minor modifications

---
 compiler/ExtractBase.ml | 36 +++++++++++++++++++++---------------
 1 file changed, 21 insertions(+), 15 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 34b5ad64..451c2c41 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -254,28 +254,34 @@ let empty_names_map : names_map =
 
 (** Small helper to report name collision *)
 let report_name_collision (id_to_string : id -> string)
-    ((id1, meta) : id * Meta.meta option) (id2 : id) (name : string) : unit =
-  let id1 = "\n- " ^ id_to_string id1 in
-  let id2 = "\n- " ^ id_to_string id2 in
+    ((id1, meta1) : id * Meta.meta option) (id2 : id) (meta2 : Meta.meta option)
+    (name : string) : unit =
+  let meta_to_string (meta : Meta.meta option) =
+    match meta with
+    | None -> ""
+    | Some meta -> "\n  " ^ Errors.meta_to_string meta.span
+  in
+  let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
+  let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
   let err =
     "Name clash detected: the following identifiers are bound to the same name \
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
   (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ meta err
+  save_error __FILE__ __LINE__ meta1 err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
     (id * Meta.meta option) option =
   StringMap.find_opt name nm.name_to_id
 
 let names_map_check_collision (id_to_string : id -> string) (id : id)
-    (name : string) (nm : names_map) : unit =
+    (meta : Meta.meta option) (name : string) (nm : names_map) : unit =
   match names_map_get_id_from_name name nm with
   | None -> () (* Ok *)
   | Some clash ->
       (* There is a clash: print a nice debugging message for the user *)
-      report_name_collision id_to_string clash id name
+      report_name_collision id_to_string clash id meta name
 
 (** Insert bindings in a names map without checking for collisions *)
 let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
@@ -289,7 +295,7 @@ let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
 let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
     (name : string) (nm : names_map) : names_map =
   (* Check if there is a clash *)
-  names_map_check_collision id_to_string id name nm;
+  names_map_check_collision id_to_string id meta name nm;
   (* Sanity check *)
   (if StringSet.mem name nm.names_set then
      let err =
@@ -385,8 +391,8 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
-    (id : id) (name : string) (nm : names_maps) : names_maps =
+let names_maps_add (id_to_string : id -> string) (id : id)
+    (meta : Meta.meta option) (name : string) (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
      type information to disambiguate field projections.
@@ -401,7 +407,7 @@ let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
   *)
   if allow_collisions id then (
     (* Check with the ids which are considered to be strict on collisions *)
-    names_map_check_collision id_to_string id name nm.strict_names_map;
+    names_map_check_collision id_to_string id meta name nm.strict_names_map;
     {
       nm with
       unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
@@ -469,21 +475,21 @@ type names_map_init = {
 
 let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (TypeId (TAssumed id)) name nm
+  names_maps_add id_to_string (TypeId (TAssumed id)) None name nm
 
 let names_maps_add_assumed_struct (id_to_string : id -> string)
     (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (StructId (TAssumed id)) name nm
+  names_maps_add id_to_string (StructId (TAssumed id)) None name nm
 
 let names_maps_add_assumed_variant (id_to_string : id -> string)
     (id : assumed_ty) (variant_id : VariantId.id) (name : string)
     (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
+  names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) None name nm
 
 let names_maps_add_function (id_to_string : id -> string)
     ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
     names_maps =
-  names_maps_add meta id_to_string (FunId fid) name nm
+  names_maps_add id_to_string (FunId fid) meta name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
 let char_name () = if !backend = Lean then "Char" else "char"
@@ -662,7 +668,7 @@ let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
   let names_maps =
-    names_maps_add (Some meta) id_to_string id name ctx.names_maps
+    names_maps_add id_to_string id (Some meta) name ctx.names_maps
   in
   { ctx with names_maps }
 
-- 
cgit v1.2.3


From eae7ce912c8bae44f98e1d489aba5618c0029bd2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 10:59:46 +0200
Subject: Make a minor modification

---
 compiler/ExtractBase.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 451c2c41..d760ab1e 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -268,8 +268,10 @@ let report_name_collision (id_to_string : id -> string)
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
-  (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ meta1 err
+  (* If we fail hard on errors, raise an exception - we don't link this error
+     to any meta information because we already put the span information about
+     the two problematic definitions in the error message above. *)
+  save_error __FILE__ __LINE__ None err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
     (id * Meta.meta option) option =
-- 
cgit v1.2.3


From f58161f23ccb4bff2080a7c63105d80777c33362 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:00:23 +0200
Subject: Update a comment

---
 compiler/ExtractBase.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index d760ab1e..f8d3cd96 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -268,9 +268,11 @@ let report_name_collision (id_to_string : id -> string)
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
-  (* If we fail hard on errors, raise an exception - we don't link this error
-     to any meta information because we already put the span information about
-     the two problematic definitions in the error message above. *)
+  (* Register the error.
+
+     We don't link this error to any meta information because we already put
+     the span information about the two problematic definitions in the error
+     message above. *)
   save_error __FILE__ __LINE__ None err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
-- 
cgit v1.2.3


From 795e2107e305d425efdf6071b29f186cae83656b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:56:09 +0200
Subject: Update the names of the synthesized backward functions

---
 compiler/ExtractBase.ml    | 6 ++++--
 compiler/SymbolicToPure.ml | 9 +++++++++
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..0a7c8df2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1662,9 +1662,11 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
   in
   (* If there is a basename, we use it *)
   match basename with
-  | Some basename ->
+  | Some basename -> (
       (* This should be a no-op *)
-      to_snake_case basename
+      match !Config.backend with
+      | Lean -> basename
+      | FStar | Coq | HOL4 -> to_snake_case basename)
   | None -> (
       (* No basename: we use the first letter of the type *)
       match ty with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 0c30f44c..7e970029 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1502,6 +1502,15 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
         match ty with None -> None | Some ty -> Some (name, ty))
       back_vars
   in
+  (* If there is one backward function or less, we use the name "back"
+     (there is no point in using the lifetime name, and it makes the
+     code generation more stable) *)
+  let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in
+  let back_vars =
+    if num_back_vars = 1 then
+      List.map (Option.map (fun (_, ty) -> (Some "back", ty))) back_vars
+    else back_vars
+  in
   fresh_opt_vars back_vars ctx
 
 (** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *)
-- 
cgit v1.2.3


From 975ddb208f18cb4ba46293dd788c46eb1ce43938 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:58:44 +0200
Subject: Regenerate the test files

---
 tests/coq/betree/BetreeMain_Funs.v                 | 12 ++--
 .../coq/betree/BetreeMain_FunsExternal_Template.v  |  3 +-
 tests/coq/demo/Demo.v                              | 28 ++++----
 tests/coq/hashmap/Hashmap_Funs.v                   | 18 ++---
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v       | 17 +++--
 tests/coq/misc/External_Funs.v                     |  4 +-
 tests/coq/misc/External_FunsExternal_Template.v    |  9 ++-
 tests/coq/misc/External_TypesExternal_Template.v   |  3 +-
 tests/coq/misc/Loops.v                             | 78 ++++++++++----------
 tests/coq/misc/NoNestedBorrows.v                   | 12 ++--
 tests/coq/misc/Paper.v                             | 12 ++--
 tests/coq/misc/PoloniusList.v                      |  4 +-
 tests/coq/traits/Traits.v                          |  3 +-
 tests/fstar/betree/BetreeMain.Funs.fst             | 12 ++--
 tests/fstar/betree/BetreeMain.FunsExternal.fsti    |  3 +-
 .../fstar/betree_back_stateful/BetreeMain.Funs.fst | 12 ++--
 .../BetreeMain.FunsExternal.fsti                   |  3 +-
 tests/fstar/demo/Demo.fst                          | 26 ++++---
 tests/fstar/hashmap/Hashmap.Funs.fst               | 17 +++--
 tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst   | 17 +++--
 tests/fstar/misc/External.Funs.fst                 |  4 +-
 tests/fstar/misc/External.FunsExternal.fsti        |  9 ++-
 tests/fstar/misc/External.TypesExternal.fsti       |  3 +-
 tests/fstar/misc/Loops.Funs.fst                    | 83 +++++++++++-----------
 tests/fstar/misc/NoNestedBorrows.fst               | 11 ++-
 tests/fstar/misc/Paper.fst                         | 11 ++-
 tests/fstar/misc/PoloniusList.fst                  |  4 +-
 tests/fstar/traits/Traits.fst                      |  3 +-
 tests/lean/BetreeMain/Funs.lean                    | 12 ++--
 tests/lean/BetreeMain/FunsExternal_Template.lean   |  3 +-
 tests/lean/Demo/Demo.lean                          | 32 ++++-----
 tests/lean/External/Funs.lean                      |  4 +-
 tests/lean/External/FunsExternal_Template.lean     |  9 ++-
 tests/lean/External/TypesExternal_Template.lean    |  3 +-
 tests/lean/Hashmap/Funs.lean                       | 16 ++---
 tests/lean/HashmapMain/Funs.lean                   | 16 ++---
 tests/lean/Loops.lean                              | 80 ++++++++++-----------
 tests/lean/NoNestedBorrows.lean                    | 16 ++---
 tests/lean/Paper.lean                              | 16 ++---
 tests/lean/PoloniusList.lean                       |  4 +-
 tests/lean/Traits.lean                             |  3 +-
 41 files changed, 322 insertions(+), 313 deletions(-)

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index c2cca26d..9256b149 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -240,11 +240,11 @@ Fixpoint betree_Node_lookup_first_message_for_key
       else (
         p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
         let (l, lookup_first_message_for_key_back) := p in
-        let back_'a :=
+        let back :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
             next_msgs1 <- lookup_first_message_for_key_back ret;
             Return (Betree_List_Cons (i, m) next_msgs1) in
-        Return (l, back_'a))
+        Return (l, back))
     | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
   end
@@ -440,11 +440,11 @@ Fixpoint betree_Node_lookup_first_message_after_key
       then (
         p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs;
         let (l, lookup_first_message_after_key_back) := p1 in
-        let back_'a :=
+        let back :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
             next_msgs1 <- lookup_first_message_after_key_back ret;
             Return (Betree_List_Cons (k, m) next_msgs1) in
-        Return (l, back_'a))
+        Return (l, back))
       else Return (Betree_List_Cons (k, m) next_msgs, Return)
     | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
@@ -550,11 +550,11 @@ Fixpoint betree_Node_lookup_mut_in_bindings
       else (
         p <- betree_Node_lookup_mut_in_bindings n1 key tl;
         let (l, lookup_mut_in_bindings_back) := p in
-        let back_'a :=
+        let back :=
           fun (ret : betree_List_t (u64 * u64)) =>
             tl1 <- lookup_mut_in_bindings_back ret;
             Return (Betree_List_Cons (i, i1) tl1) in
-        Return (l, back_'a))
+        Return (l, back))
     | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
   end
diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
index a9969448..1367bac2 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
@@ -38,7 +38,8 @@ Axiom betree_utils_store_leaf_node
 .
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
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
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index d709a8d5..67543c8e 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -376,15 +376,15 @@ Fixpoint hashMap_get_mut_in_list_loop
     | List_Cons ckey cvalue tl =>
       if ckey s= key
       then
-        let back_'a := fun (ret : T) => Return (List_Cons ckey ret tl) in
-        Return (cvalue, back_'a)
+        let back := fun (ret : T) => Return (List_Cons ckey ret tl) in
+        Return (cvalue, back)
       else (
         p <- hashMap_get_mut_in_list_loop T n1 tl key;
-        let (t, back_'a) := p in
-        let back_'a1 :=
-          fun (ret : T) =>
-            tl1 <- back_'a ret; Return (List_Cons ckey cvalue tl1) in
-        Return (t, back_'a1))
+        let (t, back) := p in
+        let back1 :=
+          fun (ret : T) => tl1 <- back ret; Return (List_Cons ckey cvalue tl1)
+          in
+        Return (t, back1))
     | List_Nil => Fail_ Failure
     end
   end
@@ -415,7 +415,7 @@ Definition hashMap_get_mut
   let (l, index_mut_back) := p in
   p1 <- hashMap_get_mut_in_list T n l key;
   let (t, get_mut_in_list_back) := p1 in
-  let back_'a :=
+  let back :=
     fun (ret : T) =>
       l1 <- get_mut_in_list_back ret;
       v <- index_mut_back l1;
@@ -426,7 +426,7 @@ Definition hashMap_get_mut
           hashMap_max_load := self.(hashMap_max_load);
           hashMap_slots := v
         |} in
-  Return (t, back_'a)
+  Return (t, back)
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 9fb3c482..a614e52d 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -398,16 +398,15 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop
     | Hashmap_List_Cons ckey cvalue tl =>
       if ckey s= key
       then
-        let back_'a := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl)
-          in
-        Return (cvalue, back_'a)
+        let back := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) in
+        Return (cvalue, back)
       else (
         p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key;
-        let (t, back_'a) := p in
-        let back_'a1 :=
+        let (t, back) := p in
+        let back1 :=
           fun (ret : T) =>
-            tl1 <- back_'a ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
-        Return (t, back_'a1))
+            tl1 <- back ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
+        Return (t, back1))
     | Hashmap_List_Nil => Fail_ Failure
     end
   end
@@ -438,7 +437,7 @@ Definition hashmap_HashMap_get_mut
   let (l, index_mut_back) := p in
   p1 <- hashmap_HashMap_get_mut_in_list T n l key;
   let (t, get_mut_in_list_back) := p1 in
-  let back_'a :=
+  let back :=
     fun (ret : T) =>
       l1 <- get_mut_in_list_back ret;
       v <- index_mut_back l1;
@@ -450,7 +449,7 @@ Definition hashmap_HashMap_get_mut
           hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
           hashmap_HashMap_slots := v
         |} in
-  Return (t, back_'a)
+  Return (t, back)
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index faf91fef..a6832854 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -46,8 +46,8 @@ Definition custom_swap
   p <- core_mem_swap T x y st;
   let (st1, p1) := p in
   let (x1, y1) := p1 in
-  let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
-  Return (st1, (x1, back_'a))
+  let back := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+  Return (st1, (x1, back))
 .
 
 (** [external::test_custom_swap]:
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 6773ac18..24dd2d47 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -12,19 +12,22 @@ Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+    Name pattern: core::mem::swap *)
 Axiom core_mem_swap :
   forall(T : Type), T -> T -> state -> result (state * (T * T))
 .
 
 (** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+    Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
 Axiom core_num_nonzero_NonZeroU32_new
   : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
 .
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
index 7ba79d8e..7d6af202 100644
--- a/tests/coq/misc/External_TypesExternal_Template.v
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -10,7 +10,8 @@ Local Open Scope Primitives_scope.
 Module External_TypesExternal_Template.
 
 (** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+    Name pattern: core::num::nonzero::NonZeroU32 *)
 Axiom core_num_nonzero_NonZeroU32_t : Type.
 
 (** The state type used in the state-error monad *)
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
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
 .
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index ad77fa2a..77276223 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -27,8 +27,8 @@ Check (test_incr )%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)
 .
 
 (** [paper::test_choose]:
@@ -70,16 +70,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
 .
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index 8f403a8e..dfa09328 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -31,10 +31,10 @@ Fixpoint get_list_at_x
     else (
       p <- get_list_at_x tl x;
       let (l, get_list_at_x_back) := p in
-      let back_'a :=
+      let back :=
         fun (ret : List_t u32) =>
           tl1 <- get_list_at_x_back ret; Return (List_Cons hd tl1) in
-      Return (l, back_'a))
+      Return (l, back))
   | List_Nil => Return (List_Nil, Return)
   end
 .
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index a861c114..0e942c7d 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -671,7 +671,8 @@ Arguments foo_x { _ _ }.
 Arguments foo_y { _ _ }.
 
 (** [core::result::Result]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+    Name pattern: core::result::Result *)
 Inductive core_result_Result_t (T E : Type) :=
 | Core_result_Result_Ok : T -> core_result_Result_t T E
 | Core_result_Result_Err : E -> core_result_Result_t T E
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 2469f98c..129e6f7e 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -195,11 +195,11 @@ let rec betree_Node_lookup_first_message_for_key
     else
       let* (l, lookup_first_message_for_key_back) =
         betree_Node_lookup_first_message_for_key key next_msgs in
-      let back_'a =
+      let back =
         fun ret ->
           let* next_msgs1 = lookup_first_message_for_key_back ret in
           Return (Betree_List_Cons (i, m) next_msgs1) in
-      Return (l, back_'a)
+      Return (l, back)
   | Betree_List_Nil -> Return (Betree_List_Nil, Return)
   end
 
@@ -352,11 +352,11 @@ let rec betree_Node_lookup_first_message_after_key
     then
       let* (l, lookup_first_message_after_key_back) =
         betree_Node_lookup_first_message_after_key key next_msgs in
-      let back_'a =
+      let back =
         fun ret ->
           let* next_msgs1 = lookup_first_message_after_key_back ret in
           Return (Betree_List_Cons (k, m) next_msgs1) in
-      Return (l, back_'a)
+      Return (l, back)
     else Return (Betree_List_Cons (k, m) next_msgs, Return)
   | Betree_List_Nil -> Return (Betree_List_Nil, Return)
   end
@@ -453,11 +453,11 @@ let rec betree_Node_lookup_mut_in_bindings
     else
       let* (l, lookup_mut_in_bindings_back) =
         betree_Node_lookup_mut_in_bindings key tl in
-      let back_'a =
+      let back =
         fun ret ->
           let* tl1 = lookup_mut_in_bindings_back ret in
           Return (Betree_List_Cons (i, i1) tl1) in
-      Return (l, back_'a)
+      Return (l, back)
   | Betree_List_Nil -> Return (Betree_List_Nil, Return)
   end
 
diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
index de9b96fd..3aad9390 100644
--- a/tests/fstar/betree/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
@@ -29,7 +29,8 @@ val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 2469f98c..129e6f7e 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -195,11 +195,11 @@ let rec betree_Node_lookup_first_message_for_key
     else
       let* (l, lookup_first_message_for_key_back) =
         betree_Node_lookup_first_message_for_key key next_msgs in
-      let back_'a =
+      let back =
         fun ret ->
           let* next_msgs1 = lookup_first_message_for_key_back ret in
           Return (Betree_List_Cons (i, m) next_msgs1) in
-      Return (l, back_'a)
+      Return (l, back)
   | Betree_List_Nil -> Return (Betree_List_Nil, Return)
   end
 
@@ -352,11 +352,11 @@ let rec betree_Node_lookup_first_message_after_key
     then
       let* (l, lookup_first_message_after_key_back) =
         betree_Node_lookup_first_message_after_key key next_msgs in
-      let back_'a =
+      let back =
         fun ret ->
           let* next_msgs1 = lookup_first_message_after_key_back ret in
           Return (Betree_List_Cons (k, m) next_msgs1) in
-      Return (l, back_'a)
+      Return (l, back)
     else Return (Betree_List_Cons (k, m) next_msgs, Return)
   | Betree_List_Nil -> Return (Betree_List_Nil, Return)
   end
@@ -453,11 +453,11 @@ let rec betree_Node_lookup_mut_in_bindings
     else
       let* (l, lookup_mut_in_bindings_back) =
         betree_Node_lookup_mut_in_bindings key tl in
-      let back_'a =
+      let back =
         fun ret ->
           let* tl1 = lookup_mut_in_bindings_back ret in
           Return (Betree_List_Cons (i, i1) tl1) in
-      Return (l, back_'a)
+      Return (l, back)
   | Betree_List_Nil -> Return (Betree_List_Nil, Return)
   end
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
index de9b96fd..3aad9390 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -29,7 +29,8 @@ val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
 
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index d93bc847..9c59ab9b 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -10,8 +10,8 @@ open Primitives
 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)
 
 (** [demo::mul2_add1]:
     Source: 'src/demo.rs', lines 13:0-13:31 *)
@@ -66,15 +66,14 @@ let rec list_nth_mut
     | CList_CCons x tl ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (CList_CCons ret tl) in
-        Return (x, back_'a)
+        let back = fun ret -> Return (CList_CCons ret tl) in Return (x, back)
       else
         let* i1 = u32_sub i 1 in
         let* (x1, list_nth_mut_back) = list_nth_mut t n1 tl i1 in
-        let back_'a =
+        let back =
           fun ret ->
             let* tl1 = list_nth_mut_back ret in Return (CList_CCons x tl1) in
-        Return (x1, back_'a)
+        Return (x1, back)
     | CList_CNil -> Fail Failure
     end
 
@@ -92,14 +91,13 @@ let rec list_nth_mut1_loop
     | CList_CCons x tl ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (CList_CCons ret tl) in
-        Return (x, back_'a)
+        let back = fun ret -> Return (CList_CCons ret tl) in Return (x, back)
       else
         let* i1 = u32_sub i 1 in
-        let* (x1, back_'a) = list_nth_mut1_loop t n1 tl i1 in
-        let back_'a1 =
-          fun ret -> let* tl1 = back_'a ret in Return (CList_CCons x tl1) in
-        Return (x1, back_'a1)
+        let* (x1, back) = list_nth_mut1_loop t n1 tl i1 in
+        let back1 =
+          fun ret -> let* tl1 = back ret in Return (CList_CCons x tl1) in
+        Return (x1, back1)
     | CList_CNil -> Fail Failure
     end
 
@@ -135,10 +133,10 @@ let rec list_tail
     begin match l with
     | CList_CCons x tl ->
       let* (c, list_tail_back) = list_tail t n1 tl in
-      let back_'a =
+      let back =
         fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1)
         in
-      Return (c, back_'a)
+      Return (c, back)
     | CList_CNil -> Return (CList_CNil, Return)
     end
 
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index fba711f1..0e770ac9 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -287,14 +287,13 @@ let rec hashMap_get_mut_in_list_loop
   | List_Cons ckey cvalue tl ->
     if ckey = key
     then
-      let back_'a = fun ret -> Return (List_Cons ckey ret tl) in
-      Return (cvalue, back_'a)
+      let back = fun ret -> Return (List_Cons ckey ret tl) in
+      Return (cvalue, back)
     else
-      let* (x, back_'a) = hashMap_get_mut_in_list_loop t tl key in
-      let back_'a1 =
-        fun ret -> let* tl1 = back_'a ret in Return (List_Cons ckey cvalue tl1)
-        in
-      Return (x, back_'a1)
+      let* (x, back) = hashMap_get_mut_in_list_loop t tl key in
+      let back1 =
+        fun ret -> let* tl1 = back ret in Return (List_Cons ckey cvalue tl1) in
+      Return (x, back1)
   | List_Nil -> Fail Failure
   end
 
@@ -320,12 +319,12 @@ let hashMap_get_mut
       (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots
       hash_mod in
   let* (x, get_mut_in_list_back) = hashMap_get_mut_in_list t l key in
-  let back_'a =
+  let back =
     fun ret ->
       let* l1 = get_mut_in_list_back ret in
       let* v = index_mut_back l1 in
       Return { self with slots = v } in
-  Return (x, back_'a)
+  Return (x, back)
 
 (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
     Source: 'src/hashmap.rs', lines 265:4-291:5 *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 97f4151f..09928620 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -305,15 +305,14 @@ let rec hashmap_HashMap_get_mut_in_list_loop
   | Hashmap_List_Cons ckey cvalue tl ->
     if ckey = key
     then
-      let back_'a = fun ret -> Return (Hashmap_List_Cons ckey ret tl) in
-      Return (cvalue, back_'a)
+      let back = fun ret -> Return (Hashmap_List_Cons ckey ret tl) in
+      Return (cvalue, back)
     else
-      let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t tl key in
-      let back_'a1 =
+      let* (x, back) = hashmap_HashMap_get_mut_in_list_loop t tl key in
+      let back1 =
         fun ret ->
-          let* tl1 = back_'a ret in Return (Hashmap_List_Cons ckey cvalue tl1)
-        in
-      Return (x, back_'a1)
+          let* tl1 = back ret in Return (Hashmap_List_Cons ckey cvalue tl1) in
+      Return (x, back1)
   | Hashmap_List_Nil -> Fail Failure
   end
 
@@ -339,12 +338,12 @@ let hashmap_HashMap_get_mut
       (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t))
       self.slots hash_mod in
   let* (x, get_mut_in_list_back) = hashmap_HashMap_get_mut_in_list t l key in
-  let back_'a =
+  let back =
     fun ret ->
       let* l1 = get_mut_in_list_back ret in
       let* v = index_mut_back l1 in
       Return { self with slots = v } in
-  Return (x, back_'a)
+  Return (x, back)
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
     Source: 'src/hashmap.rs', lines 265:4-291:5 *)
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 3ba20022..78960404 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -34,8 +34,8 @@ let custom_swap
   result (state & (t & (t -> state -> result (state & (t & t)))))
   =
   let* (st1, (x1, y1)) = core_mem_swap t x y st in
-  let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in
-  Return (st1, (x1, back_'a))
+  let back = fun ret st2 -> Return (st2, (ret, y1)) in
+  Return (st1, (x1, back))
 
 (** [external::test_custom_swap]:
     Source: 'src/external.rs', lines 29:0-29:59 *)
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index a412aea9..4c1c58b7 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -7,16 +7,19 @@ include External.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+    Name pattern: core::mem::swap *)
 val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t))
 
 (** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+    Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
 val core_num_nonzero_NonZeroU32_new
   : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
 
 (** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
 
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index 4bfbe0c5..45174c7e 100644
--- a/tests/fstar/misc/External.TypesExternal.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -6,7 +6,8 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+    Name pattern: core::num::nonzero::NonZeroU32 *)
 val core_num_nonzero_NonZeroU32_t : Type0
 
 (** The state type used in the state-error monad *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 7c099da2..93683deb 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -289,18 +289,17 @@ let rec list_nth_mut_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        let back_'b = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'a, back_'b)
+        let back'a = fun ret -> Return (List_Cons ret tl0) in
+        let back'b = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back'a, back'b)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1
-          in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        let back_'b1 =
-          fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'a1, back_'b1)
+        let* (p, back'a, back'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1 in
+        let back'a1 =
+          fun ret -> let* tl01 = back'a ret in Return (List_Cons x0 tl01) in
+        let back'b1 =
+          fun ret -> let* tl11 = back'b ret in Return (List_Cons x1 tl11) in
+        Return (p, back'a1, back'b1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -352,18 +351,18 @@ let rec list_nth_mut_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a =
+        let back =
           fun ret ->
             let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) in
-        Return ((x0, x1), back_'a)
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
+        let* (p, back) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
+        let back1 =
           fun ret ->
-            let* (tl01, tl11) = back_'a ret in
+            let* (tl01, tl11) = back ret in
             Return (List_Cons x0 tl01, List_Cons x1 tl11) in
-        Return (p, back_'a1)
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -417,14 +416,14 @@ let rec list_nth_mut_shared_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl0) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
+        let back1 =
+          fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -451,15 +450,15 @@ let rec list_nth_mut_shared_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl0) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl0) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) =
-          list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1
+          in
+        let back1 =
+          fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -486,14 +485,14 @@ let rec list_nth_shared_mut_loop_pair_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'b = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'b)
+        let back = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
-        let back_'b1 =
-          fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'b1)
+        let* (p, back) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
+        let back1 =
+          fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
@@ -520,15 +519,15 @@ let rec list_nth_shared_mut_loop_pair_merge_loop
     | List_Cons x1 tl1 ->
       if i = 0
       then
-        let back_'a = fun ret -> Return (List_Cons ret tl1) in
-        Return ((x0, x1), back_'a)
+        let back = fun ret -> Return (List_Cons ret tl1) in
+        Return ((x0, x1), back)
       else
         let* i1 = u32_sub i 1 in
-        let* (p, back_'a) =
-          list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 in
-        let back_'a1 =
-          fun ret -> let* tl11 = back_'a ret in Return (List_Cons x1 tl11) in
-        Return (p, back_'a1)
+        let* (p, back) = list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1
+          in
+        let back1 =
+          fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+        Return (p, back1)
     | List_Nil -> Fail Failure
     end
   | List_Nil -> Fail Failure
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index db63eb0d..1a93beaa 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -291,8 +291,8 @@ let _ = assert_norm (test_split_list = 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)
 
 (** [no_nested_borrows::choose_test]:
     Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 *)
@@ -355,15 +355,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
 
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
 
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index b477802b..4203247e 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -23,10 +23,10 @@ let rec get_list_at_x
     then Return (List_Cons hd tl, Return)
     else
       let* (l, get_list_at_x_back) = get_list_at_x tl x in
-      let back_'a =
+      let back =
         fun ret ->
           let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
-      Return (l, back_'a)
+      Return (l, back)
   | List_Nil -> Return (List_Nil, Return)
   end
 
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index fba564a5..199d49bf 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -503,7 +503,8 @@ let use_wrapper_len (t : Type0) (traitInst : trait_t t) : result usize =
 type foo_t (t u : Type0) = { x : t; y : u; }
 
 (** [core::result::Result]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *)
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+    Name pattern: core::result::Result *)
 type core_result_Result_t (t e : Type0) =
 | Core_result_Result_Ok : t -> core_result_Result_t t e
 | Core_result_Result_Err : e -> core_result_Result_t t e
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index ca9b48da..2fbcd6a4 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -192,12 +192,12 @@ divergent def betree.Node.lookup_first_message_for_key
       do
       let (l, lookup_first_message_for_key_back) ←
         betree.Node.lookup_first_message_for_key key next_msgs
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let next_msgs1 ← lookup_first_message_for_key_back ret
           Result.ret (betree.List.Cons (i, m) next_msgs1)
-      Result.ret (l, back_'a)
+      Result.ret (l, back)
   | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
@@ -364,12 +364,12 @@ divergent def betree.Node.lookup_first_message_after_key
       do
       let (l, lookup_first_message_after_key_back) ←
         betree.Node.lookup_first_message_after_key key next_msgs
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let next_msgs1 ← lookup_first_message_after_key_back ret
           Result.ret (betree.List.Cons (k, m) next_msgs1)
-      Result.ret (l, back_'a)
+      Result.ret (l, back)
     else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret)
   | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
 
@@ -468,12 +468,12 @@ divergent def betree.Node.lookup_mut_in_bindings
       do
       let (l, lookup_mut_in_bindings_back) ←
         betree.Node.lookup_mut_in_bindings key tl
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← lookup_mut_in_bindings_back ret
           Result.ret (betree.List.Cons (i, i1) tl1)
-      Result.ret (l, back_'a)
+      Result.ret (l, back)
   | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index eaa4b6c2..0b3e4ef4 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -29,7 +29,8 @@ axiom betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit)
 
 /- [core::option::{core::option::Option<T>}::unwrap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+   Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
 axiom core.option.Option.unwrap
   (T : Type) : Option T → State → Result (State × T)
 
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 4acc69c8..6d9fef8e 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -12,10 +12,10 @@ def choose
   Result (T × (T → Result (T × T)))
   :=
   if b
-  then let back_'a := fun ret => Result.ret (ret, y)
-       Result.ret (x, back_'a)
-  else let back_'a := fun ret => Result.ret (x, ret)
-       Result.ret (y, back_'a)
+  then let back := fun ret => Result.ret (ret, y)
+       Result.ret (x, back)
+  else let back := fun ret => Result.ret (x, ret)
+       Result.ret (y, back)
 
 /- [demo::mul2_add1]:
    Source: 'src/demo.rs', lines 13:0-13:31 -/
@@ -73,18 +73,18 @@ divergent def list_nth_mut
   | CList.CCons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (CList.CCons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ret (CList.CCons ret tl)
+      Result.ret (x, back)
     else
       do
       let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← list_nth_mut_back ret
           Result.ret (CList.CCons x tl1)
-      Result.ret (t, back_'a)
+      Result.ret (t, back)
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]: loop 0:
@@ -97,17 +97,17 @@ divergent def list_nth_mut1_loop
   | CList.CCons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (CList.CCons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ret (CList.CCons ret tl)
+      Result.ret (x, back)
     else
       do
       let i1 ← i - 1#u32
-      let (t, back_'a) ← list_nth_mut1_loop T tl i1
-      let back_'a1 :=
+      let (t, back) ← list_nth_mut1_loop T tl i1
+      let back1 :=
         fun ret => do
-                   let tl1 ← back_'a ret
+                   let tl1 ← back ret
                    Result.ret (CList.CCons x tl1)
-      Result.ret (t, back_'a1)
+      Result.ret (t, back1)
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]:
@@ -138,12 +138,12 @@ divergent def list_tail
   | CList.CCons t tl =>
     do
     let (c, list_tail_back) ← list_tail T tl
-    let back_'a :=
+    let back :=
       fun ret =>
         do
         let tl1 ← list_tail_back ret
         Result.ret (CList.CCons t tl1)
-    Result.ret (c, back_'a)
+    Result.ret (c, back)
   | CList.CNil => Result.ret (CList.CNil, Result.ret)
 
 /- Trait declaration: [demo::Counter]
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 8b645037..cfb2cb3c 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -39,8 +39,8 @@ def custom_swap
   :=
   do
   let (st1, (x1, y1)) ← core.mem.swap T x y st
-  let back_'a := fun ret st2 => Result.ret (st2, (ret, y1))
-  Result.ret (st1, (x1, back_'a))
+  let back := fun ret st2 => Result.ret (st2, (ret, y1))
+  Result.ret (st1, (x1, back))
 
 /- [external::test_custom_swap]:
    Source: 'src/external.rs', lines 29:0-29:59 -/
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index 7e237369..38151dc9 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -7,17 +7,20 @@ open Primitives
 open external
 
 /- [core::mem::swap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+   Name pattern: core::mem::swap -/
 axiom core.mem.swap
   (T : Type) : T → T → State → Result (State × (T × T))
 
 /- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+   Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/
 axiom core.num.nonzero.NonZeroU32.new
   : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
 
 /- [core::option::{core::option::Option<T>}::unwrap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+   Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
 axiom core.option.Option.unwrap
   (T : Type) : Option T → State → Result (State × T)
 
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 85fef236..84245531 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -5,7 +5,8 @@ import Base
 open Primitives
 
 /- [core::num::nonzero::NonZeroU32]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+   Name pattern: core::num::nonzero::NonZeroU32 -/
 axiom core.num.nonzero.NonZeroU32 : Type
 
 /- The state type used in the state-error monad -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 1c95f7c9..0067538e 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -287,17 +287,17 @@ divergent def HashMap.get_mut_in_list_loop
   | List.Cons ckey cvalue tl =>
     if ckey = key
     then
-      let back_'a := fun ret => Result.ret (List.Cons ckey ret tl)
-      Result.ret (cvalue, back_'a)
+      let back := fun ret => Result.ret (List.Cons ckey ret tl)
+      Result.ret (cvalue, back)
     else
       do
-      let (t, back_'a) ← HashMap.get_mut_in_list_loop T tl key
-      let back_'a1 :=
+      let (t, back) ← HashMap.get_mut_in_list_loop T tl key
+      let back1 :=
         fun ret =>
           do
-          let tl1 ← back_'a ret
+          let tl1 ← back ret
           Result.ret (List.Cons ckey cvalue tl1)
-      Result.ret (t, back_'a1)
+      Result.ret (t, back1)
   | List.Nil => Result.fail .panic
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
@@ -322,13 +322,13 @@ def HashMap.get_mut
     alloc.vec.Vec.index_mut (List T) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod
   let (t, get_mut_in_list_back) ← HashMap.get_mut_in_list T l key
-  let back_'a :=
+  let back :=
     fun ret =>
       do
       let l1 ← get_mut_in_list_back ret
       let v ← index_mut_back l1
       Result.ret { self with slots := v }
-  Result.ret (t, back_'a)
+  Result.ret (t, back)
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
    Source: 'src/hashmap.rs', lines 265:4-291:5 -/
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 6a6934b8..0bf6c641 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -302,17 +302,17 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
   | hashmap.List.Cons ckey cvalue tl =>
     if ckey = key
     then
-      let back_'a := fun ret => Result.ret (hashmap.List.Cons ckey ret tl)
-      Result.ret (cvalue, back_'a)
+      let back := fun ret => Result.ret (hashmap.List.Cons ckey ret tl)
+      Result.ret (cvalue, back)
     else
       do
-      let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T tl key
-      let back_'a1 :=
+      let (t, back) ← hashmap.HashMap.get_mut_in_list_loop T tl key
+      let back1 :=
         fun ret =>
           do
-          let tl1 ← back_'a ret
+          let tl1 ← back ret
           Result.ret (hashmap.List.Cons ckey cvalue tl1)
-      Result.ret (t, back_'a1)
+      Result.ret (t, back1)
   | hashmap.List.Nil => Result.fail .panic
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]:
@@ -338,13 +338,13 @@ def hashmap.HashMap.get_mut
       (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
       hash_mod
   let (t, get_mut_in_list_back) ← hashmap.HashMap.get_mut_in_list T l key
-  let back_'a :=
+  let back :=
     fun ret =>
       do
       let l1 ← get_mut_in_list_back ret
       let v ← index_mut_back l1
       Result.ret { self with slots := v }
-  Result.ret (t, back_'a)
+  Result.ret (t, back)
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
    Source: 'src/hashmap.rs', lines 265:4-291:5 -/
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 0f3d77c2..27434db8 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -295,22 +295,22 @@ divergent def list_nth_mut_loop_pair_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a := fun ret => Result.ret (List.Cons ret tl0)
-        let back_'b := fun ret => Result.ret (List.Cons ret tl1)
-        Result.ret ((x0, x1), back_'a, back_'b)
+        let back'a := fun ret => Result.ret (List.Cons ret tl0)
+        let back'b := fun ret => Result.ret (List.Cons ret tl1)
+        Result.ret ((x0, x1), back'a, back'b)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
+        let back'a1 :=
           fun ret => do
-                     let tl01 ← back_'a ret
+                     let tl01 ← back'a ret
                      Result.ret (List.Cons x0 tl01)
-        let back_'b1 :=
+        let back'b1 :=
           fun ret => do
-                     let tl11 ← back_'b ret
+                     let tl11 ← back'b ret
                      Result.ret (List.Cons x1 tl11)
-        Result.ret (p, back_'a1, back_'b1)
+        Result.ret (p, back'a1, back'b1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -356,21 +356,21 @@ divergent def list_nth_mut_loop_pair_merge_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a :=
+        let back :=
           fun ret =>
             let (t, t1) := ret
             Result.ret (List.Cons t tl0, List.Cons t1 tl1)
-        Result.ret ((x0, x1), back_'a)
+        Result.ret ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
+        let back1 :=
           fun ret =>
             do
-            let (tl01, tl11) ← back_'a ret
+            let (tl01, tl11) ← back ret
             Result.ret (List.Cons x0 tl01, List.Cons x1 tl11)
-        Result.ret (p, back_'a1)
+        Result.ret (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -417,17 +417,17 @@ divergent def list_nth_mut_shared_loop_pair_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a := fun ret => Result.ret (List.Cons ret tl0)
-        Result.ret ((x0, x1), back_'a)
+        let back := fun ret => Result.ret (List.Cons ret tl0)
+        Result.ret ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
+        let back1 :=
           fun ret => do
-                     let tl01 ← back_'a ret
+                     let tl01 ← back ret
                      Result.ret (List.Cons x0 tl01)
-        Result.ret (p, back_'a1)
+        Result.ret (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -451,18 +451,17 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a := fun ret => Result.ret (List.Cons ret tl0)
-        Result.ret ((x0, x1), back_'a)
+        let back := fun ret => Result.ret (List.Cons ret tl0)
+        Result.ret ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a) ←
-          list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
+        let back1 :=
           fun ret => do
-                     let tl01 ← back_'a ret
+                     let tl01 ← back ret
                      Result.ret (List.Cons x0 tl01)
-        Result.ret (p, back_'a1)
+        Result.ret (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -486,17 +485,17 @@ divergent def list_nth_shared_mut_loop_pair_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'b := fun ret => Result.ret (List.Cons ret tl1)
-        Result.ret ((x0, x1), back_'b)
+        let back := fun ret => Result.ret (List.Cons ret tl1)
+        Result.ret ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
-        let back_'b1 :=
+        let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
+        let back1 :=
           fun ret => do
-                     let tl11 ← back_'b ret
+                     let tl11 ← back ret
                      Result.ret (List.Cons x1 tl11)
-        Result.ret (p, back_'b1)
+        Result.ret (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -520,18 +519,17 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a := fun ret => Result.ret (List.Cons ret tl1)
-        Result.ret ((x0, x1), back_'a)
+        let back := fun ret => Result.ret (List.Cons ret tl1)
+        Result.ret ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a) ←
-          list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
+        let back1 :=
           fun ret => do
-                     let tl11 ← back_'a ret
+                     let tl11 ← back ret
                      Result.ret (List.Cons x1 tl11)
-        Result.ret (p, back_'a1)
+        Result.ret (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 5f9ec0f2..b90f6aef 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -331,10 +331,10 @@ def choose
   Result (T × (T → Result (T × T)))
   :=
   if b
-  then let back_'a := fun ret => Result.ret (ret, y)
-       Result.ret (x, back_'a)
-  else let back_'a := fun ret => Result.ret (x, ret)
-       Result.ret (y, back_'a)
+  then let back := fun ret => Result.ret (ret, y)
+       Result.ret (x, back)
+  else let back := fun ret => Result.ret (x, ret)
+       Result.ret (y, back)
 
 /- [no_nested_borrows::choose_test]:
    Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 -/
@@ -406,18 +406,18 @@ divergent def list_nth_mut
   | List.Cons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (List.Cons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ret (List.Cons ret tl)
+      Result.ret (x, back)
     else
       do
       let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← list_nth_mut_back ret
           Result.ret (List.Cons x tl1)
-      Result.ret (t, back_'a)
+      Result.ret (t, back)
   | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::list_rev_aux]:
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 924ff36c..5b00aa83 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -29,10 +29,10 @@ def choose
   Result (T × (T → Result (T × T)))
   :=
   if b
-  then let back_'a := fun ret => Result.ret (ret, y)
-       Result.ret (x, back_'a)
-  else let back_'a := fun ret => Result.ret (x, ret)
-       Result.ret (y, back_'a)
+  then let back := fun ret => Result.ret (ret, y)
+       Result.ret (x, back)
+  else let back := fun ret => Result.ret (x, ret)
+       Result.ret (y, back)
 
 /- [paper::test_choose]:
    Source: 'src/paper.rs', lines 23:0-23:20 -/
@@ -68,18 +68,18 @@ divergent def list_nth_mut
   | List.Cons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (List.Cons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ret (List.Cons ret tl)
+      Result.ret (x, back)
     else
       do
       let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← list_nth_mut_back ret
           Result.ret (List.Cons x tl1)
-      Result.ret (t, back_'a)
+      Result.ret (t, back)
   | List.Nil => Result.fail .panic
 
 /- [paper::sum]:
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 59c557a0..c657237f 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -24,12 +24,12 @@ divergent def get_list_at_x
     else
       do
       let (l, get_list_at_x_back) ← get_list_at_x tl x
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← get_list_at_x_back ret
           Result.ret (List.Cons hd tl1)
-      Result.ret (l, back_'a)
+      Result.ret (l, back)
   | List.Nil => Result.ret (List.Nil, Result.ret)
 
 end polonius_list
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index acddd1a9..766b109d 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -512,7 +512,8 @@ structure Foo (T U : Type) where
   y : U
 
 /- [core::result::Result]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+   Name pattern: core::result::Result -/
 inductive core.result.Result (T E : Type) :=
 | Ok : T → core.result.Result T E
 | Err : E → core.result.Result T E
-- 
cgit v1.2.3


From bac38f94aacf4a0d621b0b2d2c423db9e0c6f175 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:21:08 +0200
Subject: Improve the name of the backward functions further

---
 compiler/PureUtils.ml      | 11 ++++++++---
 compiler/SymbolicToPure.ml | 13 +++++++++++--
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 4bc90872..6f44bb74 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -75,10 +75,15 @@ let inputs_info_is_wf (info : inputs_info) : bool =
 let fun_sig_info_is_wf (info : fun_sig_info) : bool =
   inputs_info_is_wf info.fwd_info
 
+let opt_dest_arrow_ty (ty : ty) : (ty * ty) option =
+  match ty with TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) | _ -> None
+
+let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty)
+
 let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty =
-  match ty with
-  | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
-  | _ -> craise __FILE__ __LINE__ meta "Not an arrow type"
+  match opt_dest_arrow_ty ty with
+  | Some (arg_ty, ret_ty) -> (arg_ty, ret_ty)
+  | None -> craise __FILE__ __LINE__ meta "Not an arrow type"
 
 let compute_literal_type (cv : literal) : literal_type =
   match cv with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7e970029..67fd2c9b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1499,7 +1499,14 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
   let back_vars =
     List.map
       (fun (name, ty) ->
-        match ty with None -> None | Some ty -> Some (name, ty))
+        match ty with
+        | None -> None
+        | Some ty ->
+            (* If the type is not an arrow type, don't use the name "back"
+               (it is a backward function with no inputs, that is to say a
+               value) *)
+            let name = if is_arrow_ty ty then name else None in
+            Some (name, ty))
       back_vars
   in
   (* If there is one backward function or less, we use the name "back"
@@ -1508,7 +1515,9 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
   let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in
   let back_vars =
     if num_back_vars = 1 then
-      List.map (Option.map (fun (_, ty) -> (Some "back", ty))) back_vars
+      List.map
+        (Option.map (fun (name, ty) -> (Option.map (fun _ -> "back") name, ty)))
+        back_vars
     else back_vars
   in
   fresh_opt_vars back_vars ctx
-- 
cgit v1.2.3


From 46f64c1b9f3bfc2703186b32a74c611e0e43f63f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:21:47 +0200
Subject: Regenerate the test files

---
 tests/coq/hashmap/Hashmap_Funs.v                 | 12 ++++++------
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v     | 12 ++++++------
 tests/fstar/hashmap/Hashmap.Funs.fst             | 12 ++++++------
 tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 12 ++++++------
 tests/lean/Hashmap/Funs.lean                     | 12 ++++++------
 tests/lean/HashmapMain/Funs.lean                 | 12 ++++++------
 6 files changed, 36 insertions(+), 36 deletions(-)

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 67543c8e..c0cde78d 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -94,13 +94,13 @@ Fixpoint hashMap_clear_loop
     Source: 'src/hashmap.rs', lines 80:4-80:27 *)
 Definition hashMap_clear
   (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) :=
-  back <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
+  hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
   Return
     {|
       hashMap_num_entries := 0%usize;
       hashMap_max_load_factor := self.(hashMap_max_load_factor);
       hashMap_max_load := self.(hashMap_max_load);
-      hashMap_slots := back
+      hashMap_slots := hm
     |}
 .
 
@@ -125,8 +125,8 @@ Fixpoint hashMap_insert_in_list_loop
       then Return (false, List_Cons ckey value tl)
       else (
         p <- hashMap_insert_in_list_loop T n1 key value tl;
-        let (b, back) := p in
-        Return (b, List_Cons ckey cvalue back))
+        let (b, tl1) := p in
+        Return (b, List_Cons ckey cvalue tl1))
     | List_Nil => Return (true, List_Cons key value List_Nil)
     end
   end
@@ -450,8 +450,8 @@ Fixpoint hashMap_remove_from_list_loop
         end
       else (
         p <- hashMap_remove_from_list_loop T n1 key tl;
-        let (o, back) := p in
-        Return (o, List_Cons ckey t back))
+        let (o, tl1) := p in
+        Return (o, List_Cons ckey t tl1))
     | List_Nil => Return (None, List_Nil)
     end
   end
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index a614e52d..8e299800 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -104,13 +104,13 @@ Definition hashmap_HashMap_clear
   (T : Type) (n : nat) (self : hashmap_HashMap_t T) :
   result (hashmap_HashMap_t T)
   :=
-  back <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
+  hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
   Return
     {|
       hashmap_HashMap_num_entries := 0%usize;
       hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor);
       hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
-      hashmap_HashMap_slots := back
+      hashmap_HashMap_slots := hm
     |}
 .
 
@@ -136,8 +136,8 @@ Fixpoint hashmap_HashMap_insert_in_list_loop
       then Return (false, Hashmap_List_Cons ckey value tl)
       else (
         p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl;
-        let (b, back) := p in
-        Return (b, Hashmap_List_Cons ckey cvalue back))
+        let (b, tl1) := p in
+        Return (b, Hashmap_List_Cons ckey cvalue tl1))
     | Hashmap_List_Nil =>
       Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
     end
@@ -474,8 +474,8 @@ Fixpoint hashmap_HashMap_remove_from_list_loop
         end
       else (
         p <- hashmap_HashMap_remove_from_list_loop T n1 key tl;
-        let (o, back) := p in
-        Return (o, Hashmap_List_Cons ckey t back))
+        let (o, tl1) := p in
+        Return (o, Hashmap_List_Cons ckey t tl1))
     | Hashmap_List_Nil => Return (None, Hashmap_List_Nil)
     end
   end
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 0e770ac9..d897933a 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -79,8 +79,8 @@ let rec hashMap_clear_loop
 (** [hashmap::{hashmap::HashMap<T>}::clear]:
     Source: 'src/hashmap.rs', lines 80:4-80:27 *)
 let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) =
-  let* back = hashMap_clear_loop t self.slots 0 in
-  Return { self with num_entries = 0; slots = back }
+  let* hm = hashMap_clear_loop t self.slots 0 in
+  Return { self with num_entries = 0; slots = hm }
 
 (** [hashmap::{hashmap::HashMap<T>}::len]:
     Source: 'src/hashmap.rs', lines 90:4-90:30 *)
@@ -99,8 +99,8 @@ let rec hashMap_insert_in_list_loop
     if ckey = key
     then Return (false, List_Cons ckey value tl)
     else
-      let* (b, back) = hashMap_insert_in_list_loop t key value tl in
-      Return (b, List_Cons ckey cvalue back)
+      let* (b, tl1) = hashMap_insert_in_list_loop t key value tl in
+      Return (b, List_Cons ckey cvalue tl1)
   | List_Nil -> Return (true, List_Cons key value List_Nil)
   end
 
@@ -344,8 +344,8 @@ let rec hashMap_remove_from_list_loop
       | List_Nil -> Fail Failure
       end
     else
-      let* (o, back) = hashMap_remove_from_list_loop t key tl in
-      Return (o, List_Cons ckey x back)
+      let* (o, tl1) = hashMap_remove_from_list_loop t key tl in
+      Return (o, List_Cons ckey x tl1)
   | List_Nil -> Return (None, List_Nil)
   end
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 09928620..e0005c81 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -84,8 +84,8 @@ let rec hashmap_HashMap_clear_loop
     Source: 'src/hashmap.rs', lines 80:4-80:27 *)
 let hashmap_HashMap_clear
   (t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) =
-  let* back = hashmap_HashMap_clear_loop t self.slots 0 in
-  Return { self with num_entries = 0; slots = back }
+  let* hm = hashmap_HashMap_clear_loop t self.slots 0 in
+  Return { self with num_entries = 0; slots = hm }
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
     Source: 'src/hashmap.rs', lines 90:4-90:30 *)
@@ -105,8 +105,8 @@ let rec hashmap_HashMap_insert_in_list_loop
     if ckey = key
     then Return (false, Hashmap_List_Cons ckey value tl)
     else
-      let* (b, back) = hashmap_HashMap_insert_in_list_loop t key value tl in
-      Return (b, Hashmap_List_Cons ckey cvalue back)
+      let* (b, tl1) = hashmap_HashMap_insert_in_list_loop t key value tl in
+      Return (b, Hashmap_List_Cons ckey cvalue tl1)
   | Hashmap_List_Nil ->
     Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
   end
@@ -364,8 +364,8 @@ let rec hashmap_HashMap_remove_from_list_loop
       | Hashmap_List_Nil -> Fail Failure
       end
     else
-      let* (o, back) = hashmap_HashMap_remove_from_list_loop t key tl in
-      Return (o, Hashmap_List_Cons ckey x back)
+      let* (o, tl1) = hashmap_HashMap_remove_from_list_loop t key tl in
+      Return (o, Hashmap_List_Cons ckey x tl1)
   | Hashmap_List_Nil -> Return (None, Hashmap_List_Nil)
   end
 
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 0067538e..363d751a 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -79,8 +79,8 @@ divergent def HashMap.clear_loop
    Source: 'src/hashmap.rs', lines 80:4-80:27 -/
 def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
-  let back ← HashMap.clear_loop T self.slots 0#usize
-  Result.ret { self with num_entries := 0#usize, slots := back }
+  let hm ← HashMap.clear_loop T self.slots 0#usize
+  Result.ret { self with num_entries := 0#usize, slots := hm }
 
 /- [hashmap::{hashmap::HashMap<T>}::len]:
    Source: 'src/hashmap.rs', lines 90:4-90:30 -/
@@ -99,8 +99,8 @@ divergent def HashMap.insert_in_list_loop
     then Result.ret (false, List.Cons ckey value tl)
     else
       do
-      let (b, back) ← HashMap.insert_in_list_loop T key value tl
-      Result.ret (b, List.Cons ckey cvalue back)
+      let (b, tl1) ← HashMap.insert_in_list_loop T key value tl
+      Result.ret (b, List.Cons ckey cvalue tl1)
   | List.Nil => Result.ret (true, List.Cons key value List.Nil)
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
@@ -345,8 +345,8 @@ divergent def HashMap.remove_from_list_loop
       | List.Nil => Result.fail .panic
     else
       do
-      let (o, back) ← HashMap.remove_from_list_loop T key tl
-      Result.ret (o, List.Cons ckey t back)
+      let (o, tl1) ← HashMap.remove_from_list_loop T key tl
+      Result.ret (o, List.Cons ckey t tl1)
   | List.Nil => Result.ret (none, List.Nil)
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 0bf6c641..6fac6940 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -83,8 +83,8 @@ divergent def hashmap.HashMap.clear_loop
 def hashmap.HashMap.clear
   (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
   do
-  let back ← hashmap.HashMap.clear_loop T self.slots 0#usize
-  Result.ret { self with num_entries := 0#usize, slots := back }
+  let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize
+  Result.ret { self with num_entries := 0#usize, slots := hm }
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
    Source: 'src/hashmap.rs', lines 90:4-90:30 -/
@@ -103,8 +103,8 @@ divergent def hashmap.HashMap.insert_in_list_loop
     then Result.ret (false, hashmap.List.Cons ckey value tl)
     else
       do
-      let (b, back) ← hashmap.HashMap.insert_in_list_loop T key value tl
-      Result.ret (b, hashmap.List.Cons ckey cvalue back)
+      let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl
+      Result.ret (b, hashmap.List.Cons ckey cvalue tl1)
   | hashmap.List.Nil =>
     Result.ret (true, hashmap.List.Cons key value hashmap.List.Nil)
 
@@ -364,8 +364,8 @@ divergent def hashmap.HashMap.remove_from_list_loop
       | hashmap.List.Nil => Result.fail .panic
     else
       do
-      let (o, back) ← hashmap.HashMap.remove_from_list_loop T key tl
-      Result.ret (o, hashmap.List.Cons ckey t back)
+      let (o, tl1) ← hashmap.HashMap.remove_from_list_loop T key tl
+      Result.ret (o, hashmap.List.Cons ckey t tl1)
   | hashmap.List.Nil => Result.ret (none, hashmap.List.Nil)
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]:
-- 
cgit v1.2.3


From eaab34bbf040d6b1fa8e4730ef1ea31cc0225c99 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:22:40 +0200
Subject: Update the README

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index df7b2bf1..74de4500 100644
--- a/README.md
+++ b/README.md
@@ -9,9 +9,9 @@ Wall in Pompei, digital image from Michael Lahanis.
 </figcaption>
 </div></p>
 
-# Aeneas
+# Aeneas [Ae-ne-as]
 
-Aeneas is a verification toolchain for Rust programs.  It relies on a translation from Rusts's MIR
+Aeneas (pronunced [Ae-ne-as]) is a verification toolchain for Rust programs.  It relies on a translation from Rusts's MIR
 internal language to a pure lamdba calculus.  It is intended to be used in combination with
 [Charon](https://github.com/AeneasVerif/charon), which compiles Rust programs to an intermediate
 representation called LLBC. It currently has backends for [F\*](https://www.fstar-lang.org),
-- 
cgit v1.2.3


From ec7a1d3c94846a94481a487dd077efb6ddb108fe Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:27:02 +0200
Subject: Make a minor update in SymbolicToPure

---
 compiler/SymbolicToPure.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 67fd2c9b..5cd13072 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2258,15 +2258,14 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                  (fun ty ->
                    match ty with
                    | None -> None
-                   | Some (back_sg, ty) ->
-                       (* We insert a name for the variable only if the function
-                          can fail: if it can fail, it means the call returns a backward
-                          function. Otherwise, it directly returns the value given
-                          back by the backward function, which means we shouldn't
-                          give it a name like "back..." (it doesn't make sense) *)
+                   | Some (_back_sg, ty) ->
+                       (* We insert a name for the variable only if the type
+                          is an arrow type. If it is not, it means the backward
+                          function is degenerate (it takes no inputs) so it is
+                          not a function anymore but a value: it doesn't make
+                          sense to use a name like "back...". *)
                        let name =
-                         if back_sg.effect_info.can_fail then Some back_fun_name
-                         else None
+                         if is_arrow_ty ty then Some back_fun_name else None
                        in
                        Some (name, ty))
                  back_tys)
-- 
cgit v1.2.3


From 0c3be2a82205d2737546c7ce8b15b6ad07f34095 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 14:18:32 +0200
Subject: Update the nix flake

---
 flake.lock | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/flake.lock b/flake.lock
index 5f61cb95..27a555ad 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1710913200,
-        "narHash": "sha256-TPkIajgXl7narf/2U16y+EVwrjozQed3yDrg6MJdoXo=",
+        "lastModified": 1712233083,
+        "narHash": "sha256-KR4UwlgUzLWObSzQ1LIKITjRrYe4AuZXdvCK78qrip8=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "827ee91c945717ca19ae9c3d1cdfa591d0d5e0d9",
+        "rev": "6e31313fdfd4830aa0fc795f6ab8b27600fcbbfb",
         "type": "github"
       },
       "original": {
-- 
cgit v1.2.3