Remove special declaration of primitive projections in the kernel.

This reduces kernel bloat and removes code from the TCB, as compatibility
projections are now retypechecked as normal definitions would have been.
This should have no effect on efficiency as this only happens once at
definition time.

3 files changed, 25 insertions, 40 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index bc2d2068a..39c83f47e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -382,17 +382,33 @@ let inInductive : inductive_obj -> obj =
     discharge_function = discharge_inductive;
     rebuild_function = infer_inductive_subtyping }
 
-let declare_projections mind =
+let declare_projections univs mind =
   let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
     match spec.mind_record with
-    | Some (Some (_, kns, pjs)) ->
-      Array.iteri (fun i kn ->
+    | Some (Some (_, kns, pbs)) ->
+      Array.iter2 (fun kn pb ->
 	let id = Label.to_id (Constant.label kn) in
-	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
-	let kn' = declare_constant id (ProjectionEntry entry,
-				       IsDefinition StructureComponent)
-	in
-	  assert(Constant.equal kn kn')) kns; true,true
+        let univs = match univs with
+        | Monomorphic_ind_entry _ ->
+          (** Global constraints already defined through the inductive *)
+          Monomorphic_const_entry Univ.ContextSet.empty
+        | Polymorphic_ind_entry ctx ->
+          Polymorphic_const_entry ctx
+        | Cumulative_ind_entry ctx ->
+          Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+        in
+        let term, types = match univs with
+        | Monomorphic_const_entry _ -> pb.proj_eta
+        | Polymorphic_const_entry ctx ->
+          let u = Univ.UContext.instance ctx in
+          let term, types = pb.proj_eta in
+          Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
+        in
+        let entry = definition_entry ~types ~univs term in
+        let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+        assert (Constant.equal kn kn')
+      ) kns pbs;
+      true, true
     | Some None -> true,false
     | None -> false,false
 
@@ -403,7 +419,7 @@ let declare_mind mie =
     | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   let mind = Global.mind_of_delta_kn kn in
-  let isrecord,isprim = declare_projections mind in
+  let isrecord,isprim = declare_projections mie.mind_entry_universes mind in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   oname, isprim
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 94da00c7e..3c555f8c7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *)
 type parameter_entry = 
     Context.Named.t option * types in_constant_universes_entry * inline
 
-type projection_entry = {
-  proj_entry_ind : MutInd.t;
-  proj_entry_arg : int }
-
 type 'a constant_entry =
   | DefinitionEntry of 'a definition_entry
   | ParameterEntry of parameter_entry
-  | ProjectionEntry of projection_entry
 
 (** {6 Modules } *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index d29f2ca82..37bf679c5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -346,32 +346,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
-  | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
-    let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
-    let kn, pb = 
-      match mib.mind_record with
-      | Some (Some (id, kns, pbs)) -> 
-	if i < Array.length pbs then
-	  kns.(i), pbs.(i)
-	else assert false
-      | _ -> assert false
-    in
-    let univs =
-      match mib.mind_universes with
-      | Monomorphic_ind ctx -> Monomorphic_const ctx
-      | Polymorphic_ind auctx -> Polymorphic_const auctx
-      | Cumulative_ind acumi ->
-        Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
-    in
-    let term, typ = pb.proj_eta in
-    {
-      Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term));
-      cook_type = typ;
-      cook_universes = univs;
-      cook_inline = false;
-      cook_context = None;
-    }
-
 let record_aux env s_ty s_bo =
   let in_ty = keep_hyps env s_ty in
   let v =