Quoted terms do not use primitive projections

[Tragicus]

When we introduce a term using quotations, it gets introduced using the compatibility constant of primitive projections, rather than the primitive projections themselves.

From elpi Require Import elpi.

Set Primitive Projections.
Structure S := { sort : Type; pt : sort }.

Elpi Command foo.
Section Dummy.
Variable (s : S).

Elpi Query foo lp:{{
  coq.say {{ sort s }}.
}}.

(* app [global (const «sort»), global (const «s»)] *)

Let x := sort s.

Elpi Query foo lp:{{
  global (const C) = {{ x }},
  coq.env.const-body C (some X),
  coq.say X
}}.

(* app [primitive (proj test.sort 0), global (const «s»)] *)

End Dummy.