Regenerate the test files and fix a proof

2 files changed, 15 insertions, 5 deletions

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index e950ba0b..054880d4 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -190,10 +190,6 @@ Definition hash_map_insert_no_resize_fwd_back
       |})
 .
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
 (** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hash_map_move_elements_from_list_loop_fwd_back
@@ -259,7 +255,7 @@ Definition hash_map_move_elements_fwd_back
     (there is a single backward function, and the forward function returns ()) *)
 Definition hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
-  max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+  max_usize <- scalar_cast U32 Usize core_u32_max;
   let capacity := vec_len (List_t T) self.(Hash_map_slots) in
   n1 <- usize_div max_usize 2%usize;
   let (i, i0) := self.(Hash_map_max_load_factor) in
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y)  (at level 80) : Primitives_scope.
 Notation "x s>= y" := (scalar_geb x y)  (at level 80) : Primitives_scope.
 Notation "x s> y" := (scalar_gtb x y)  (at level 80) : Primitives_scope.
 
+(** Constants *)
+Definition core_u8_max    := u8_max %u32.
+Definition core_u16_max   := u16_max %u32.
+Definition core_u32_max   := u32_max %u32.
+Definition core_u64_max   := u64_max %u64.
+Definition core_u128_max  := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max    := i8_max %i32.
+Definition core_i16_max   := i16_max %i32.
+Definition core_i32_max   := i32_max %i32.
+Definition core_i64_max   := i64_max %i64.
+Definition core_i128_max  := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
 (*** Range *)
 Record range (T : Type) := mk_range {
   start: T;