Merge branch 'main' into son/loops2

8 files changed, 6 insertions, 6 deletions

diff --git a/tests/hol4/hashmap_on_disk/Holmakefile b/tests/hol4/constants/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/hashmap_on_disk/Holmakefile
+++ b/tests/hol4/constants/Holmakefile
diff --git a/tests/hol4/misc-external/Holmakefile b/tests/hol4/hashmap_main/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-external/Holmakefile
+++ b/tests/hol4/hashmap_main/Holmakefile
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
index c1e30aa6..2a17d185 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
@@ -628,9 +628,9 @@ val insert_on_disk_fwd_def = Define ‘
   insert_on_disk_fwd
     (key : usize) (value : u64) (st : state) : (state # unit) result =
     do
-    (st0, hm) <- hashmap_utils_deserialize_fwd st;
+    (st0, hm) <- utils_deserialize_fwd st;
     hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
-    (st1, _) <- hashmap_utils_serialize_fwd hm0 st0;
+    (st1, _) <- utils_serialize_fwd hm0 st0;
     Return (st1, ())
     od
 ’
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
index d4e43d9a..c19673bb 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
@@ -583,9 +583,9 @@ sig
       ⊢ ∀key value st.
           insert_on_disk_fwd key value st =
           do
-            (st0,hm) <- hashmap_utils_deserialize_fwd st;
+            (st0,hm) <- utils_deserialize_fwd st;
             hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
-            (st1,_) <- hashmap_utils_serialize_fwd hm0 st0;
+            (st1,_) <- utils_serialize_fwd hm0 st0;
             Return (st1,())
           od
    
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
index f7221d92..9c29c0e0 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
@@ -6,10 +6,10 @@ open hashmapMain_TypesTheory
 val _ = new_theory "hashmapMain_Opaque"
 
 
-(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd",
+(** [hashmap_main::utils::deserialize]: forward function *)val _ = new_constant ("utils_deserialize_fwd",
   “:state -> (state # u64 hashmap_hash_map_t) result”)
 
-(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd",
+(** [hashmap_main::utils::serialize]: forward function *)val _ = new_constant ("utils_serialize_fwd",
   “:u64 hashmap_hash_map_t -> state -> (state # unit) result”)
 
 val _ = export_theory ()
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig b/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig
index f7373609..f7373609 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml b/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml
index 3f8ca9b9..3f8ca9b9 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig b/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig
index a3e770ea..a3e770ea 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig