Merge pull request #497 from VojtechStep/feature/breaking-add-section-variable

Feature/breaking add section variable

Author: gares

.nix/config.nix

@@ -30,10 +30,11 @@
       paramcoq.override.version = "master";
       coqeal.job = false;  # broken in master, c.f. https://github.com/coq/coq/pull/19228
     };
-    "coq-master".ocamlPackages = { elpi.override.version = "2.0.6"; };
+    "coq-master".ocamlPackages = { elpi.override.version = "2.0.7"; };
 
     "coq-8.20".coqPackages = mcHBcommon // {
       coq.override.version = "8.20";
+      ocamlPackages = { elpi.override.version = "2.0.7"; };
     };
 
     "coq-8.19".coqPackages = mcHBcommon // {

.nix/coq-overlays/coq-elpi/default.nix

@@ -67,7 +67,7 @@ let
       {
         case = "8.20";
         out = {
-          version = "1.19.2";
+          version = "2.0.7";
         };
       }
     ] { }

HB/common/log.elpi

@@ -71,7 +71,12 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [
 pred env.add-section-variable-noimplicits i:id, i:term, o:constant.
 env.add-section-variable-noimplicits Name Ty C :- std.do! [
   if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
+% elpi:if version coq-elpi < 2.4.0
   @local! => coq.env.add-section-variable ID Ty C,
+% elpi:endif
+% elpi:if version coq-elpi >= 2.4.0
+  @local! => coq.env.add-section-variable ID _ Ty C,
+% elpi:endif
   log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
   @local! => arguments.set-implicit (const C) [[]],
 ].