diff options
Diffstat (limited to 'tests/coq')
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 12 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 12 |
2 files changed, 12 insertions, 12 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 |