We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 2560ad0 commit 5b0cea5Copy full SHA for 5b0cea5
elpi/coq-lib.elpi
@@ -510,6 +510,7 @@ coq.term->gref (global GR) GR :- !.
510
coq.term->gref (pglobal GR _) GR :- !.
511
coq.term->gref (app [Hd|_]) GR :- !, coq.term->gref Hd GR.
512
coq.term->gref (let _ _ T x\x) GR :- !, coq.term->gref T GR.
513
+coq.term->gref (primitive (proj Proj _)) GR :- !, primitive-projection? Proj GR.
514
:name "term->gref:fail"
515
coq.term->gref Term _ :-
516
fatal-error-w-data "term->gref: input has no global reference" Term.
0 commit comments