Merge PR #7714: Remove primitive-projection related data from the kernel

20 files changed, 176 insertions, 124 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 7ec345768..3304b032e 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -211,8 +211,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
-  proj_eta : constr * constr; (* Eta-expanded term and type *)
-  proj_body : constr; (* For compatibility, the match version *)
 }
 
 type constant_def =
@@ -241,7 +239,6 @@ type constant_body = {
     const_type : constr;
     const_body_code : to_patch_substituted;
     const_universes : constant_universes;
-    const_proj : bool;
     const_inline_code : bool;
     const_typing_flags : typing_flags;
 }
diff --git a/checker/environ.ml b/checker/environ.ml
index 809150cea..3d5fac806 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -166,9 +166,6 @@ let evaluable_constant cst env =
   try let _  = constant_value env (cst, Univ.Instance.empty) in true
   with Not_found | NotEvaluableConst _ -> false
 
-let is_projection cst env = 
-  (lookup_constant cst env).const_proj
-
 let lookup_projection p env =
   Cmap_env.find (Projection.constant p) env.env_globals.env_projections
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 4a7597249..acb29d7d2 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -58,7 +58,6 @@ exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> Constant.t puniverses -> constr
 val evaluable_constant : Constant.t -> env -> bool
 
-val is_projection : Constant.t -> env -> bool
 val lookup_projection : Projection.t -> env -> projection_body
 
 (* Inductives *)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 5c672d04a..f4ae02084 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -130,9 +130,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (==) (fun x -> x.proj_npars);
     check (==) (fun x -> x.proj_arg);
     check (eq_constr) (fun x -> x.proj_type);
-    check (eq_constr) (fun x -> fst x.proj_eta);
-    check (eq_constr) (fun x -> snd x.proj_eta);
-    check (eq_constr) (fun x -> x.proj_body); true
+    true
   in
   let check_inductive_type t1 t2 =
 
diff --git a/checker/values.ml b/checker/values.ml
index 67032bd1b..45f04f88d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli
+MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli
 
 *)
 
@@ -225,9 +225,7 @@ let v_cst_def =
 
 let v_projbody =
   v_tuple "projection_body"
-	  [|v_cst;Int;Int;v_constr;
-	    v_tuple "proj_eta" [|v_constr;v_constr|];
-	    v_constr|]
+    [|v_cst;Int;Int;v_constr|]
 
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
@@ -241,7 +239,6 @@ let v_cb = v_tuple "constant_body"
     Any;
     v_const_univs;
     v_bool;
-    v_bool;
     v_typing_flags|]
 
 let v_recarg = v_sum "recarg" 1 (* Norec *)
diff --git a/interp/declare.ml b/interp/declare.ml
index bc2d2068a..aa737239b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -382,17 +382,34 @@ let inInductive : inductive_obj -> obj =
     discharge_function = discharge_inductive;
     rebuild_function = infer_inductive_subtyping }
 
-let declare_projections mind =
-  let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
+let declare_projections univs mind =
+  let env = Global.env () in
+  let spec,_ = Inductive.lookup_mind_specif env (mind,0) in
     match spec.mind_record with
-    | Some (Some (_, kns, pjs)) ->
-      Array.iteri (fun i kn ->
+    | Some (Some (_, kns, _)) ->
+      let projs = Inductiveops.compute_projections env (mind, 0) in
+      Array.iter2 (fun kn (term, types) ->
 	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 _ -> term, types
+        | Polymorphic_const_entry ctx ->
+          let u = Univ.UContext.instance ctx 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 projs;
+      true, true
     | Some None -> true,false
     | None -> false,false
 
@@ -403,7 +420,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/cooking.ml b/kernel/cooking.ml
index 5783453e6..68057b389 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -156,7 +156,6 @@ type inline = bool
 type result = {
   cook_body : constant_def;
   cook_type : types;
-  cook_proj : bool;
   cook_universes : constant_universes;
   cook_inline : inline;
   cook_context : Context.Named.t option;
@@ -230,7 +229,6 @@ let cook_constant ~hcons env { from = cb; info } =
   {
     cook_body = body;
     cook_type = typ;
-    cook_proj = cb.const_proj;
     cook_universes = univs;
     cook_inline = cb.const_inline_code;
     cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0d907f3de..76c79335f 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,6 @@ type inline = bool
 type result = {
   cook_body : constant_def;
   cook_type : types;
-  cook_proj : bool;
   cook_universes : constant_universes;
   cook_inline : inline;
   cook_context : Context.Named.t option;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd70c050..7bd7d6c9c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -54,8 +54,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
-  proj_eta : constr * types; (* Eta-expanded term and type *)
-  proj_body : constr; (* For compatibility with VMs only, the match version *)
 }
 
 (* Global declarations (i.e. constants) can be either: *)
@@ -87,7 +85,6 @@ type constant_body = {
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
-    const_proj : bool;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 75c0e5b4c..1b73096f7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -86,7 +86,7 @@ let subst_const_def sub def = match def with
 let subst_const_proj sub pb =
   { pb with proj_ind = subst_mind sub pb.proj_ind;
     proj_type = subst_mps sub pb.proj_type;
-    proj_body = subst_const_type sub pb.proj_body }
+  }
 
 let subst_const_body sub cb =
   assert (List.is_empty cb.const_hyps); (* we're outside sections *)
@@ -100,7 +100,6 @@ let subst_const_body sub cb =
       { const_hyps = [];
         const_body = body';
         const_type = type';
-        const_proj = cb.const_proj;
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
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/environ.ml b/kernel/environ.ml
index fb89576dd..2d6c9117b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -490,7 +490,7 @@ let lookup_projection cst env =
   Cmap_env.find (Projection.constant cst) env.env_globals.env_projections
 
 let is_projection cst env =
-  (lookup_constant cst env).const_proj
+  Cmap_env.mem cst env.env_globals.env_projections
 
 (* Mutual Inductives *)
 let polymorphic_ind (mind,i) env =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 439acd15b..14f2a3d8f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -797,16 +797,13 @@ exception UndefinableExpansion
     build an expansion function.
     The term built is expecting to be substituted first by 
     a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+let compute_projections ((kn, _ as ind), u) nparamargs params
     mind_consnrealdecls mind_consnrealargs paramslet ctx =
   let mp, dp, l = MutInd.repr3 kn in
   (** We build a substitution smashing the lets in the record parameters so
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
-  let indty, paramsletsubst =
-    (* [ty] = [Ind inst] is typed in context [params] *)
-    let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
-    let ty = mkApp (mkIndU indu, inst) in
+  let paramsletsubst =
     (* [Ind inst] is typed in context [params-wo-let] *)
     let inst' = rel_list 0 nparamargs in
     (* {params-wo-let |- subst:params] *)
@@ -814,48 +811,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
     let subst = (* For the record parameter: *)
       mkRel 1 :: List.map (lift 1) subst in
-      ty, subst
+    subst
   in
-  let ci = 
-    let print_info =
-      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
-      { ci_ind     = ind;
-	ci_npar    = nparamargs;
-	ci_cstr_ndecls = mind_consnrealdecls;
-	ci_cstr_nargs = mind_consnrealargs;
-	ci_pp_info = print_info }
-  in
-  let len = List.length ctx in
-  let x = Name x in
-  let compat_body ccl i = 
-    (* [ccl] is defined in context [params;x:indty] *)
-    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
-    let ccl' = liftn 1 2 ccl in
-    let p = mkLambda (x, lift 1 indty, ccl') in
-    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
-    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
-      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
-  in
-  let projections decl (i, j, kns, pbs, subst, letsubst) =
+  let projections decl (i, j, kns, pbs, letsubst) =
     match decl with
     | LocalDef (na,c,t) ->
         (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
            to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
         let c = liftn 1 j c in
         (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
-           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
-        let c1 = substl subst c in
-        (* From [params, x:I |- subst:field1,..,fieldj]
-           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
-           is represented with instance of field1 last *)
-        let subst = c1 :: subst in
-        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
            to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
         let c2 = substl letsubst c in
         (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
            to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
         let letsubst = c2 :: letsubst in
-        (i, j+1, kns, pbs, subst, letsubst)
+        (i, j+1, kns, pbs, letsubst)
     | LocalAssum (na,t) ->
       match na with
       | Name id ->
@@ -868,21 +838,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
 	let projty = substl letsubst t in
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
-	let ty = substl subst t in
-	let term = mkProj (Projection.make kn true, mkRel 1) in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
-	let compat = compat_body ty (j - 1) in
-	let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
-	let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
-		     proj_arg = i; proj_type = projty; proj_eta = etab, etat; 
-		     proj_body = compat } in
-	  (i + 1, j + 1, kn :: kns, body :: pbs,
-	   fterm :: subst, fterm :: letsubst)
+                      proj_arg = i; proj_type = projty; } in
+        (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, kns, pbs, subst, letsubst) =
-    List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+  let (_, _, kns, pbs, letsubst) =
+    List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
   in
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
@@ -987,7 +950,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 	(try 
 	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
-	     compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt
+             compute_projections indsp nparamargs paramsctxt
 	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
 	   in Some (Some (rid, kns, projs))
 	 with UndefinableExpansion -> Some None)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5a38172c2..45228e35e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,7 +43,7 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct
 val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
-val compute_projections : pinductive -> Id.t -> Id.t ->
+val compute_projections : pinductive ->
   int -> Context.Rel.t -> int array -> int array -> 
   Context.Rel.t -> Context.Rel.t -> 
   (Constant.t array * projection_body array)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index db1109e75..37bf679c5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = Undef nl;
         cook_type = t;
-        cook_proj = false;
         cook_universes = univs;
         cook_inline = false;
         cook_context = ctx;
@@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = def;
         cook_type = typ;
-        cook_proj = false;
         cook_universes = Monomorphic_const univs;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -343,39 +341,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = def;
         cook_type = typ;
-        cook_proj = false;
         cook_universes = univs;
         cook_inline = c.const_entry_inline_code;
         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_proj = true;
-      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 =
@@ -464,7 +434,6 @@ let build_constant_declaration kn env result =
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
-    const_proj = result.cook_proj;
     const_body_code = tps;
     const_universes = univs;
     const_inline_code = result.cook_inline;
diff --git a/library/heads.ml b/library/heads.ml
index 3d5f6a6ff..d9d650ac0 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -129,7 +129,7 @@ let compute_head = function
    let cb = Environ.lookup_constant cst env in
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
-     if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body
+     if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body
      then Global.body_of_constant cst else None
    in
      (match body with
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5aee70194..3a61c7747 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1065,11 +1065,15 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
 	  | Def c ->
-	     (match cb.const_proj with
+             (match Environ.is_projection kn env with
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                mk_typ (EConstr.of_constr pb.proj_body))
+                (** FIXME: handle mutual records *)
+                let ind = (pb.Declarations.proj_ind, 0) in
+                let bodies = Inductiveops.legacy_match_projection env ind in
+                let body = bodies.(pb.Declarations.proj_arg) in
+                mk_typ (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
             if access_opaque () then mk_typ (get_opaque env c)
@@ -1078,11 +1082,15 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
 	  | Def c ->
-	     (match cb.const_proj with
+             (match Environ.is_projection kn env with
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                mk_def (EConstr.of_constr pb.proj_body))
+                (** FIXME: handle mutual records *)
+                let ind = (pb.Declarations.proj_ind, 0) in
+                let bodies = Inductiveops.legacy_match_projection env ind in
+                let body = bodies.(pb.Declarations.proj_arg) in
+                mk_def (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
             if access_opaque () then mk_def (get_opaque env c)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df89d9eac..5a54c6f05 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t =
 	  let c' = 
 	    try 
 	      let pb = Environ.lookup_projection p (snd env) in
-	      let body = pb.Declarations.proj_body in
+              (** FIXME: handle mutual records *)
+              let ind = (pb.Declarations.proj_ind, 0) in
+              let bodies = Inductiveops.legacy_match_projection (snd env) ind in
+              let body = bodies.(pb.Declarations.proj_arg) in
 	      let ty = Retyping.get_type_of (snd env) sigma c in
 	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
 	      let body' = strip_lam_assum body in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b1ab2d2b7..1a790be64 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -454,6 +454,110 @@ let build_branch_type env sigma dep p cs =
 
 (**************************************************)
 
+(** From a rel context describing the constructor arguments,
+    build an expansion function.
+    The term built is expecting to be substituted first by
+    a substitution of the form [params, x : ind params] *)
+let compute_projections env (kn, _ as ind) =
+  let open Term in
+  let mib = Environ.lookup_mind kn env in
+  let indu = match mib.mind_universes with
+  | Monomorphic_ind _ -> mkInd ind
+  | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx)
+  | Cumulative_ind ctx ->
+    mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
+  in
+  let x = match mib.mind_record with
+  | None | Some None ->
+    anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+  | Some (Some (id, _, _)) -> Name id
+  in
+  (** FIXME: handle mutual records *)
+  let pkt = mib.mind_packets.(0) in
+  let { mind_consnrealargs; mind_consnrealdecls } = pkt in
+  let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
+  let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in
+  let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
+  let mp, dp, l = MutInd.repr3 kn in
+  (** We build a substitution smashing the lets in the record parameters so
+      that typechecking projections requires just a substitution and not
+      matching with a parameter context. *)
+  let indty =
+    (* [ty] = [Ind inst] is typed in context [params] *)
+    let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+    let ty = mkApp (indu, inst) in
+    (* [Ind inst] is typed in context [params-wo-let] *)
+    ty
+  in
+  let ci =
+    let print_info =
+      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+      { ci_ind     = ind;
+        ci_npar    = nparamargs;
+        ci_cstr_ndecls = mind_consnrealdecls;
+        ci_cstr_nargs = mind_consnrealargs;
+        ci_pp_info = print_info }
+  in
+  let len = List.length ctx in
+  let compat_body ccl i =
+    (* [ccl] is defined in context [params;x:indty] *)
+    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
+    let ccl' = liftn 1 2 ccl in
+    let p = mkLambda (x, lift 1 indty, ccl') in
+    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
+    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
+      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
+  in
+  let projections decl (j, pbs, subst) =
+    match decl with
+    | LocalDef (na,c,t) ->
+        (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
+        let c = liftn 1 j c in
+        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
+        let c1 = substl subst c in
+        (* From [params, x:I |- subst:field1,..,fieldj]
+           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
+           is represented with instance of field1 last *)
+        let subst = c1 :: subst in
+        (j+1, pbs, subst)
+    | LocalAssum (na,t) ->
+      match na with
+      | Name id ->
+        let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+        (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
+        let t = liftn 1 j t in
+        (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
+        (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
+           to [params, x:I |- t(proj1 x,..,projj x)] *)
+        let ty = substl subst t in
+        let term = mkProj (Projection.make kn true, mkRel 1) in
+        let fterm = mkProj (Projection.make kn false, mkRel 1) in
+        let compat = compat_body ty (j - 1) in
+        let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+        let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
+        let body = (etab, etat, compat) in
+        (j + 1, body :: pbs, fterm :: subst)
+      | Anonymous ->
+        anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+  in
+  let (_, pbs, subst) =
+    List.fold_right projections ctx (1, [], [])
+  in
+  Array.rev_of_list pbs
+
+let legacy_match_projection env ind =
+  Array.map pi3 (compute_projections env ind)
+
+let compute_projections ind mib =
+  let ans = compute_projections ind mib in
+  Array.map (fun (prj, ty, _) -> (prj, ty)) ans
+
+(**************************************************)
+
 let extract_mrectype sigma t =
   let open EConstr in
   let (t, l) = decompose_app sigma t in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b0d714b03..aa53f7e67 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,6 +194,18 @@ val make_case_or_project :
 val make_default_case_info : env -> case_style -> inductive -> case_info
 i*)
 
+val compute_projections : Environ.env -> inductive -> (constr * types) array
+(** Given a primitive record type, for every field computes the eta-expanded
+    projection and its type. *)
+
+val legacy_match_projection : Environ.env -> inductive -> constr array
+(** Given a record type, computes the legacy match-based projection of the
+    projections.
+
+    BEWARE: such terms are ill-typed, and should thus only be used in upper
+    layers. The kernel will probably badly fail if presented with one of
+    those. *)
+
 (********************)
 
 val type_of_inductive_knowing_conclusion :