From 54afbf3a8b71ee729641ee3024d19aaf8fa92a67 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Jun 2023 16:10:20 +0200
Subject: Start setting up the Nix derivation for HOL4

---
 backends/hol4/divDefNoFixLib.sml       | 2 +-
 backends/hol4/primitivesBaseTacLib.sml | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

(limited to 'backends')

diff --git a/backends/hol4/divDefNoFixLib.sml b/backends/hol4/divDefNoFixLib.sml
index f7b9763d..85a1b1a8 100644
--- a/backends/hol4/divDefNoFixLib.sml
+++ b/backends/hol4/divDefNoFixLib.sml
@@ -206,7 +206,7 @@ fun get_smallest_unique_id_for_names (names : string list) : string =
       handle HOL_ERR _ => false
     val _ =
       while !continue do (
-        let val _ = (continue := not (forall name_is_ok names)) in
+        let val _ = (continue := not (all name_is_ok names)) in
         if !continue then incr_i () else () end
       )
   in
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index f256d330..c079bcf1 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -17,6 +17,14 @@ val gsym = GSYM
  *)
 fun ignore_tac (_ : thm) : tactic = ALL_TAC
 
+(* REMARK: the last github version of HOL4 defines some functions which seem
+   to be absent from the last release version (which is older). As a consequence,
+   the Nix flake fails if we don't redefine those here.
+ *)
+val pop_last_assum = last_x_assum
+val qexists = qexists_tac
+(* END OF REMARK *)
+
 val pop_ignore_tac = pop_assum ignore_tac
 
 (* TODO: no exfalso tactic?? *)
-- 
cgit v1.2.3