No Projection.constant in projection <-> constant declaration

Enabled by previous commit about Heads.

3 files changed, 11 insertions, 12 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index a9bfe8cabb..1e972d3e35 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -358,10 +358,6 @@ let inInductive : mutual_inductive_entry -> obj =
 
 let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
   let id = Label.to_id label in
-  let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
-  Recordops.declare_primitive_projection p;
-  (* ^ needs to happen before declaring the constant, otherwise
-     Heads gets confused. *)
   let univs = match univs with
     | Monomorphic_ind_entry _ ->
       (** Global constraints already defined through the inductive *)
@@ -378,7 +374,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
       Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
   in
   let entry = definition_entry ~types ~univs term in
-  ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent))
+  let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+  let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
+  Recordops.declare_primitive_projection p cst
+
 
 let declare_projections univs mind =
   let env = Global.env () in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 4faa753dfb..fe9b69dbbc 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -106,16 +106,16 @@ let find_projection = function
 let prim_table =
   Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
 
-let load_prim i (_,p) =
-  prim_table := Cmap_env.add (Projection.Repr.constant p) p !prim_table
+let load_prim i (_,(p,c)) =
+  prim_table := Cmap_env.add c p !prim_table
 
 let cache_prim p = load_prim 1 p
 
-let subst_prim (subst,p) = subst_proj_repr subst p
+let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c
 
-let discharge_prim (_,p) = Some (Lib.discharge_proj_repr p)
+let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
 
-let inPrim : Projection.Repr.t -> obj =
+let inPrim : (Projection.Repr.t * Constant.t) -> obj =
   declare_object {
     (default_object "PRIMPROJS") with
     cache_function = cache_prim ;
@@ -124,7 +124,7 @@ let inPrim : Projection.Repr.t -> obj =
     classify_function = (fun x -> Substitute x);
     discharge_function = discharge_prim }
 
-let declare_primitive_projection p = Lib.add_anonymous_leaf (inPrim p)
+let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
 
 let is_primitive_projection c = Cmap_env.mem c !prim_table
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 415b964168..3e43372b65 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -45,7 +45,7 @@ val find_projection_nparams : GlobRef.t -> int
 val find_projection : GlobRef.t -> struc_typ
 
 (** Sets up the mapping from constants to primitive projections *)
-val declare_primitive_projection : Projection.Repr.t -> unit
+val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit
 
 val is_primitive_projection : Constant.t -> bool