From 53adf30fe440eb8b6f58ba89f4a4c0acc7877498 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Jun 2023 17:26:08 +0200
Subject: Add a comment

---
 backends/hol4/primitivesBaseTacLib.sml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'backends/hol4')

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
-- 
cgit v1.2.3