Add "coq.env.query-extra-dep" external predicate

LPCIC · Oct 21, 2023 · ace0641 · ace0641
1 parent c865bcf
commit ace0641
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
@@ -901,6 +901,10 @@ external pred coq.env.projections i:inductive, o:list (option constant).
 external pred coq.env.primitive-projections i:inductive, 
                                             o:list (option (pair projection int)).
 
+% [coq.env.query-extra-dep Identifier File Name] Resolve the file name of an
+% Extra Dependency
+external pred coq.env.query-extra-dep i:id, o:option id.
+
 % -- Sorts (and their universe level, if applicable) ----------------
 
 % Warning: universe polymorphism has to be considered experimental *E* as

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -2325,6 +2325,15 @@ denote the same x as before.|};
             Some (c, np + na))))))),
   DocAbove);
 
+  MLCode(Pred("coq.env.query-extra-dep",
+    In(id, "Identifier",
+    Out(option id, "File Name",
+    Easy "Resolve the file name of an Extra Dependency")),
+  (fun id _ ~depth ->
+    !: (try Some (ComExtraDeps.query_extra_dep (Names.Id.of_string id))
+        with Not_found -> None))),
+  DocAbove);
+
   LPDoc "-- Sorts (and their universe level, if applicable) ----------------";
   LPDoc {|Warning: universe polymorphism has to be considered experimental *E* as
 a feature, not just as a set of APIs. Unfortunately some of the