summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap_on_disk
diff options
context:
space:
mode:
authorSon Ho2023-01-13 16:18:43 +0100
committerSon HO2023-02-03 11:21:46 +0100
commite69382acbcc4bdd27612c9cf8ec282db71f8408d (patch)
tree61d2ab1565d1d8ee083308a92f05e547e0583f98 /tests/coq/hashmap_on_disk
parent6de775cde92e37f2e5e70d3db34a326a4c831920 (diff)
Improve the pretty names generation for loops
Diffstat (limited to 'tests/coq/hashmap_on_disk')
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v12
1 files changed, 6 insertions, 6 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 94a9e6a5..670e527a 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -139,8 +139,8 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_back
if ckey s= key
then Return (HashmapListCons ckey value tl)
else (
- l <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl;
- Return (HashmapListCons ckey cvalue l))
+ tl0 <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl;
+ Return (HashmapListCons ckey cvalue tl0))
| HashmapListNil =>
let l := HashmapListNil in Return (HashmapListCons key value l)
end
@@ -391,8 +391,8 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
if ckey s= key
then Return (HashmapListCons ckey ret tl)
else (
- l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret;
- Return (HashmapListCons ckey cvalue l))
+ tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret;
+ Return (HashmapListCons ckey cvalue tl0))
| HashmapListNil => Fail_ Failure
end
end
@@ -490,8 +490,8 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back
| HashmapListNil => Fail_ Failure
end
else (
- l <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl;
- Return (HashmapListCons ckey t l))
+ tl0 <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl;
+ Return (HashmapListCons ckey t tl0))
| HashmapListNil => Return HashmapListNil
end
end