Merge pull request #605 from rlepigre/br/api-fixes

Fix a couple of bugs.
LPCIC · Feb 29, 2024 · 363f4dc · 363f4dc
2 parents 0066a3a + 7407611
commit 363f4dc
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi
@@ -608,9 +608,9 @@ coq.with-TC Class Instance->Clause Code :-
 
 pred coq.replay-synterp-action i:synterp-action.
 coq.replay-synterp-action (begin-module ID) :- coq.env.begin-module ID _.
-coq.replay-synterp-action (end-module _) :- coq.env.end-module _.
+coq.replay-synterp-action (end-module MP) :- coq.env.end-module MP.
 coq.replay-synterp-action (begin-module-type ID) :- coq.env.begin-module-type ID.
-coq.replay-synterp-action (end-module-type _) :- coq.env.end-module-type _.
+coq.replay-synterp-action (end-module-type MTP) :- coq.env.end-module-type MTP.
 coq.replay-synterp-action (apply-module-functor ID) :- coq.env.apply-module-functor ID _ _ _ _ _.
 coq.replay-synterp-action (apply-module-type-functor ID) :- coq.env.apply-module-type-functor ID _ _ _ _.
 coq.replay-synterp-action (include-module MP) :- coq.env.include-module MP _.

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -1855,7 +1855,12 @@ Supported attributes:
      state, !: s, [])),
   DocAbove);
 
-  Coq_elpi_builtins_synterp.current_path;
+  MLCode(Pred("coq.env.current-path",
+    Out(list B.string, "Path",
+    Read(unit_ctx, "lists the current module path")),
+  (fun _ ~depth _ _ state -> !: (mp2path (Global.current_modpath ())))),
+  DocAbove);
+
   Coq_elpi_builtins_synterp.current_section_path;
 
   LPCode {|% Deprecated, use coq.env.opaque?