diff options
author | Son Ho | 2023-01-13 16:18:43 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | e69382acbcc4bdd27612c9cf8ec282db71f8408d (patch) | |
tree | 61d2ab1565d1d8ee083308a92f05e547e0583f98 /tests/fstar/hashmap_on_disk | |
parent | 6de775cde92e37f2e5e70d3db34a326a4c831920 (diff) |
Improve the pretty names generation for loops
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index d2b87305..f3b480c3 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -137,7 +137,7 @@ let rec hashmap_hash_map_insert_in_list_loop_back else begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with | Fail e -> Fail e - | Return l -> Return (HashmapListCons ckey cvalue l) + | Return tl0 -> Return (HashmapListCons ckey cvalue tl0) end | HashmapListNil -> let l = HashmapListNil in Return (HashmapListCons key value l) @@ -442,7 +442,7 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back else begin match hashmap_hash_map_get_mut_in_list_loop_back t tl key ret with | Fail e -> Fail e - | Return l -> Return (HashmapListCons ckey cvalue l) + | Return tl0 -> Return (HashmapListCons ckey cvalue tl0) end | HashmapListNil -> Fail Failure end @@ -553,7 +553,7 @@ let rec hashmap_hash_map_remove_from_list_loop_back else begin match hashmap_hash_map_remove_from_list_loop_back t key tl with | Fail e -> Fail e - | Return l -> Return (HashmapListCons ckey x l) + | Return tl0 -> Return (HashmapListCons ckey x tl0) end | HashmapListNil -> Return HashmapListNil end |