Update the Makefile and regenerate some tests

1 files changed, 12 insertions, 0 deletions

diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 47cdc3af..e916ca4a 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -71,6 +71,18 @@ Definition div_test1 (x : u32) : result u32 :=
 Definition rem_test (x : u32) (y : u32) : result u32 :=
   u32_rem x y.
 
+(** [no_nested_borrows::mul_test]: forward function *)
+Definition mul_test (x : u32) (y : u32) : result u32 :=
+  u32_mul x y.
+
+(** [no_nested_borrows::CONST0] *)
+Definition const0_body : result usize := usize_add 1%usize 1%usize.
+Definition const0_c : usize := const0_body%global.
+
+(** [no_nested_borrows::CONST1] *)
+Definition const1_body : result usize := usize_mul 2%usize 2%usize.
+Definition const1_c : usize := const1_body%global.
+
 (** [no_nested_borrows::cast_test]: forward function *)
 Definition cast_test (x : u32) : result i32 :=
   scalar_cast U32 I32 x.