Regenerate the hashmap code and update the proofs

2 files changed, 2 insertions, 7 deletions

diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 90390c1b..b5476f25 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -46,10 +46,7 @@ Definition test_new_non_zero_u32_fwd
 
 (** [external::test_vec] *)
 Definition test_vec_fwd : result unit :=
-  let v := vec_new u32 in
-  v0 <- vec_push_back u32 v (0%u32);
-  let _ := v0 in
-  Return tt
+  let v := vec_new u32 in _ <- vec_push_back u32 v (0%u32); Return tt
 .
 
 (** Unit test for [external::test_vec] *)
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index e91cf81a..10654887 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -67,9 +67,7 @@ Definition rem_test_fwd (x : u32) (y : u32) : result u32 := u32_rem x y.
 Definition cast_test_fwd (x : u32) : result i32 := scalar_cast U32 I32 x.
 
 (** [no_nested_borrows::test2] *)
-Definition test2_fwd : result unit :=
-  i <- u32_add 23%u32 44%u32; let _ := i in Return tt
-.
+Definition test2_fwd : result unit := _ <- u32_add 23%u32 44%u32; Return tt.
 
 (** Unit test for [no_nested_borrows::test2] *)
 Check (test2_fwd )%return.