From 8ac12ccdd3e55b8da910c6c8b7bb8dff94a6a640 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 Jan 2023 19:18:18 +0100
Subject: Regenerate the hashmap code and update the proofs

---
 tests/coq/misc/External_Funs.v   | 5 +----
 tests/coq/misc/NoNestedBorrows.v | 4 +---
 2 files changed, 2 insertions(+), 7 deletions(-)

(limited to 'tests/coq/misc')

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.
-- 
cgit v1.2.3