add primitive proj LPCIC#792

Author: FissoreD

apps/tc/elpi/ho_compile.elpi

@@ -23,6 +23,7 @@ namespace tc {
         decompile-term-aux (pglobal _ _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
+        decompile-term-aux (primitive _ as P) L P L :- !.
 
         decompile-term-aux (tc.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !,
           name Y X S,

apps/tc/elpi/ho_precompile.elpi

@@ -142,7 +142,7 @@ namespace tc {
       %   precompile-aux IsP Ty A Ty1 A1, pi x\ is-name x => precompile-aux IsP (F x) A1 (F1 x) A2.
       % precompile-aux IsP (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
       %   precompile-aux IsP T A T1 A1, precompile-aux IsP Rty A1 Rty1 A2, std.fold-map B A2 (precompile-aux IsP) B1 A3.
-      % precompile-aux _ (primitive _ as C) A C A :- !.
+      precompile-aux _ (primitive _ as C) A C A :- !.
       % precompile-aux IsP (uvar M L as X) A W A1 :- var X, !, std.fold-map L A (precompile-aux IsP) L1 A1, coq.mk-app-uvar M L1 W.
       % % when used in CHR rules
       % precompile-aux IsP (uvar X L) A (uvar X L1) A1 :- std.fold-map L A (precompile-aux IsP) L1 A1.

apps/tc/tests/prim_proj.v

@@ -0,0 +1,9 @@
+From elpi Require Import tc.
+
+Set Primitive Projections.
+Record S := { sort :> Type }.
+Unset Primitive Projections.
+
+Class C (s : Type) := {}.
+
+Instance SC (s : S) : C s := Build_C s.