summaryrefslogtreecommitdiff
path: root/backends/hol4/primitivesBaseTacLib.sml
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4/primitivesBaseTacLib.sml')
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml10
1 files changed, 7 insertions, 3 deletions
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index c079bcf1..943a25b5 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -17,9 +17,13 @@ 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.
+(* REMARK: the last github version of HOL4 defines some functions which are
+ absent from the last **release** version (which is older). We redefine some of
+ them here for convenience.
+
+ IMPORTANT: in practice, we use the last *release* version of HOL4 (i.e., not
+ the last *development* version) to make sure that building the Nix flake
+ succeeds (there *are* discrepancies of behavior).
*)
val pop_last_assum = last_x_assum
val qexists = qexists_tac