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/coq/hashmap_on_disk | |
parent | 6de775cde92e37f2e5e70d3db34a326a4c831920 (diff) |
Improve the pretty names generation for loops
Diffstat (limited to '')
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 12 |
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 |