Revert "[TC] compilation of primitive projections to their compatibil…

…ity constants"

This reverts commit 6c63978.

apps/tc/elpi/ho_compile.elpi

@@ -23,7 +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 (proj P _)) L (global (const Y)) L :- !, coq.env.primitive-projection? P Y.
+        decompile-term-aux (primitive _ as X) L X L :- !.
         decompile-term-aux (tc.canonical-projection T S _) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
           name Y X S,
           decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
@@ -334,8 +334,7 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      decompile-problematic-term (primitive (proj P _)) A (global (const Y)) A :- !, 
-        coq.env.primitive-projection? P Y.
+      decompile-problematic-term (primitive _ as C) A C A :- !.
 
       decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :-
         prune V S, !, fold-map T L T' L2.

apps/tc/tests/canonical_struct.v

@@ -99,23 +99,4 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
-
-Module CS6.
-  #[projections(primitive=yes)]
-  Structure ofe := Ofe { ofe_car : Type; }.
-
-  #[projections(primitive=no)] (* TODO: Putting primitive to yes leads to a unification error. Why? *)
-  Structure cmra := { cmra_car :> Type; }.
-  Canonical Structure cmra_ofeO (A : cmra) : ofe := Ofe A.
-
-  Class C (I : Type).
-  Instance c : forall (A : ofe), C ((A).(ofe_car)) := {}.
-
-  Section s.
-    Context {cmra : cmra}.
-    Goal C (cmra_car cmra).
-      apply _.
-    Qed.
-  End s.
-End CS6.
+End CS5.