diff options
| author | Son Ho | 2023-06-02 17:26:08 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | 53adf30fe440eb8b6f58ba89f4a4c0acc7877498 (patch) | |
| tree | 1d31d111bc373af8a0df1f7a72f6a77e4aedec3a | |
| parent | dc46dbb9a01329c39673fedc195006745c365030 (diff) | |
Add a comment
| -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 |