summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap_on_disk
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/hashmap_on_disk')
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst6
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