diff options
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 10 |
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 |