Merge PR #8781: Remove primproj <-> constant dependency in Heads

4 files changed, 21 insertions, 31 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/heads.ml b/pretyping/heads.ml
index a3e4eb8971..e533930267 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -26,9 +26,8 @@ open Context.Named.Declaration
    the evaluation of [phi(0)] and the head of [h] is declared unknown). *)
 
 type rigid_head_kind =
-| RigidParameter of Constant.t (* a Const without body *)
-| RigidVar of variable (* a Var without body *)
-| RigidType (* an inductive, a product or a sort *)
+| RigidParameter of Constant.t (* a Const without body. Module substitution may instantiate it with something else. *)
+| RigidOther (* a Var without body, inductive, product, sort, projection *)
 
 type head_approximation =
 | RigidHead of rigid_head_kind
@@ -77,7 +76,7 @@ let kind_of_head env t =
                str "."))
   | Construct _ | CoFix _ ->
       if b then NotImmediatelyComputableHead else ConstructorHead
-  | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
+  | Sort _ | Ind _ | Prod _ -> RigidHead RigidOther
   | Cast (c,_,_) -> aux k l c b
   | Lambda (_,_,c) ->
     begin match l with
@@ -89,9 +88,7 @@ let kind_of_head env t =
   | LetIn _ -> assert false
   | Meta _ | Evar _ -> NotImmediatelyComputableHead
   | App (c,al) -> aux k (Array.to_list al @ l) c b
-  | Proj (p,c) ->
-      (try on_subterm k (c :: l) b (constant_head (Projection.constant p))
-       with Not_found -> assert false)
+  | Proj (p,c) -> RigidHead RigidOther
 
   | Case (_,_,c,_) -> aux k [] c true
   | Fix ((i,j),_) ->
@@ -124,22 +121,16 @@ let kind_of_head env t =
 (* FIXME: maybe change interface here *)
 let compute_head = function
 | EvalConstRef cst ->
-   let env = Global.env() in
-   let cb = Environ.lookup_constant cst env in
-   let is_Def = function Declarations.Def _ -> true | _ -> false in
-   let body =
-     if not (Recordops.is_primitive_projection cst) && is_Def cb.Declarations.const_body
-     then Global.body_of_constant cst else None
-   in
-     (match body with
-     | None -> RigidHead (RigidParameter cst)
-     | Some (c, _) -> kind_of_head env c)
+  let env = Global.env() in
+  let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in
+  (match body with
+   | None -> RigidHead (RigidParameter cst)
+   | Some c -> kind_of_head env c)
 | EvalVarRef id ->
     (match Global.lookup_named id with
      | LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
            kind_of_head (Global.env()) c
-     | _ ->
-           RigidHead (RigidVar id))
+     | _ -> RigidHead RigidOther)
 
 let is_rigid env t =
   match kind_of_head env t with
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