declare compatibility constant as canonical gref for primitive projec…

…tions
LPCIC · Mar 4, 2025 · 9559572 · 9559572
1 parent 2560ad0
commit 9559572
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi
@@ -510,6 +510,7 @@ coq.term->gref (global GR) GR :- !.
 coq.term->gref (pglobal GR _) GR :- !.
 coq.term->gref (app [Hd|_]) GR :- !, coq.term->gref Hd GR.
 coq.term->gref (let _ _ T x\x) GR :- !, coq.term->gref T GR.
+coq.term->gref (primitive (proj Proj _)) GR :- !, coq.projection->gref Proj GR.
 :name "term->gref:fail"
 coq.term->gref Term _ :-
   fatal-error-w-data "term->gref: input has no global reference" Term.

diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml
@@ -3954,6 +3954,13 @@ coq.id->name S N :- coq.string->name S N.
   (fun gr _ ~depth h c state -> !: (gr2path gr))),
   DocAbove);
 
+  MLCode(Pred("coq.projection->gref",
+    In(projection, "Proj",
+    Out(gref, "GR",
+    Read(unit_ctx, "extract the name of the compatibility constant associated to Proj"))),
+  (fun p _ ~depth h c state -> !: (GlobRef.ConstRef (Projection.constant p)))),
+  DocAbove);
+
   Rocq_elpi_builtins_synterp.modpath_to_path;
   Rocq_elpi_builtins_synterp.modtypath_to_path;
   Rocq_elpi_builtins_synterp.modpath_to_library;