From 5b0cea57cc72f3d1b25128c32b20d481cfaf4a10 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 4 Mar 2025 11:45:06 +0100 Subject: [PATCH 1/2] declare compatibility constant as canonical gref for primitive projections --- elpi/coq-lib.elpi | 1 + 1 file changed, 1 insertion(+) diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi index fb834b161..908e14280 100644 --- 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 :- !, primitive-projection? Proj GR. :name "term->gref:fail" coq.term->gref Term _ :- fatal-error-w-data "term->gref: input has no global reference" Term. From 10ebb1fa2e455b411180a50ddb3d6dff2ba7c8ab Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 4 Mar 2025 16:23:38 +0100 Subject: [PATCH 2/2] typo --- elpi/coq-lib.elpi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi index 908e14280..cab6a55d3 100644 --- a/elpi/coq-lib.elpi +++ b/elpi/coq-lib.elpi @@ -510,7 +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 :- !, primitive-projection? Proj GR. +coq.term->gref (primitive (proj Proj _)) (const C) :- coq.env.primitive-projection? Proj C, !. :name "term->gref:fail" coq.term->gref Term _ :- fatal-error-w-data "term->gref: input has no global reference" Term.