add index to primitive-projection?

Author: Tragicus

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 _)) (const C) :- coq.env.primitive-projection? Proj C, !.
+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.

src/rocq_elpi_builtins.ml

@@ -929,7 +929,7 @@ let add_axiom_or_variable api id ty local_bkind options state =
     | None -> begin
       Dumpglob.dump_definition name false "ax";
       comAssumption_declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~kind (EConstr.to_constr sigma ty)
-        ~univs ~impargs ~inline:options.inline ~name
+        ~univs ~impargs ~inline:options.inline ~name:id
       end
   in
   let ucsts = match univs with UState.Monomorphic_entry x, _ -> x | _ -> Univ.ContextSet.empty in
@@ -2363,14 +2363,15 @@ denote the same x as before.|};
   MLCode(Pred("coq.env.primitive-projection?",
     InOut(B.ioarg projection, "Projection",
     InOut(B.ioarg constant, "Compatibility constant",
-    Read(global, "Relates a primitive projection to its compatibility constant."))),
-    (fun p c ~depth coq_context _ _ ->
+    Out(int, "Index",
+    Read(global, "Relates a primitive projection to its compatibility constant and its index in the record.")))),
+    (fun p c _ ~depth coq_context _ _ ->
       match p, c with
       | _, Data (Variable c) -> raise No_clause
       | Data p, Data (Constant c) ->
-          if Constant.equal (Projection.constant p) c then ?: None +? None else raise No_clause
+          if Constant.equal (Projection.constant p) c then ?: None +? None +! Names.Projection.(arg p + npars p) else raise No_clause
       | NoData, NoData -> U.type_error "coq.env.primitive-projection?: got no input data"
-      | Data p, NoData -> ?: None +! (Constant (Projection.constant p))
+      | Data p, NoData -> ?: None +! (Constant (Projection.constant p)) +! Names.Projection.(arg p + npars p)
       | NoData, Data (Constant c) ->
           (match Environ.constant_opt_value_in coq_context.env (UVars.in_punivs c) with
           | None -> raise No_clause
@@ -2381,7 +2382,9 @@ denote the same x as before.|};
               | App (hd, _) -> get_proj hd
               | Proj (p, _, _) -> p
               | _ -> raise No_clause
-            in !: (get_proj p) +? None))),
+            in
+            let p = get_proj p in
+            !: p +? None +! Names.Projection.(arg p + npars p)))),
   DocAbove);
 
   LPDoc "-- Sorts (and their universe level, if applicable) ----------------";

tests/test_HOAS.v

@@ -221,7 +221,7 @@ Module P''.
 
   Elpi Query  lp:{{
     app[primitive (proj P _) | _] = {{X.(proj1 _)}},
-    coq.env.primitive-projection? P C,
+    coq.env.primitive-projection? P C _,
     global (const C) = {{proj1}}.
   }}.