Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.

21 files changed, 182 insertions, 168 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index cb0fc32575..3758008189 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -71,7 +71,7 @@ and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
   | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
-  | PROJ of Projection.t * Declarations.projection_body * cbv_stack
+  | PROJ of Projection.t * cbv_stack
 
 (* les vars pourraient etre des constr,
    cela permet de retarder les lift: utile ?? *)
@@ -126,7 +126,7 @@ let rec stack_concat stk1 stk2 =
       TOP -> stk2
     | APP(v,stk1') -> APP(v,stack_concat stk1' stk2)
     | CASE(c,b,i,s,stk1') -> CASE(c,b,i,s,stack_concat stk1' stk2)
-    | PROJ (p,pinfo,stk1') -> PROJ (p,pinfo,stack_concat stk1' stk2)
+    | PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2)
 
 (* merge stacks when there is no shifts in between *)
 let mkSTACK = function
@@ -200,7 +200,7 @@ let rec reify_stack t = function
       reify_stack
         (mkCase (ci, ty, t,br))
         st
-  | PROJ (p, pinfo, st) ->
+  | PROJ (p, st) ->
        reify_stack (mkProj (p, t)) st
 
 and reify_value = function (* reduction under binders *)
@@ -265,8 +265,7 @@ let rec norm_head info env t stack =
       then Projection.unfold p
       else p
     in 
-    let pinfo = Environ.lookup_projection p (info_env info.infos) in
-      norm_head info env c (PROJ (p', pinfo, stack))
+      norm_head info env c (PROJ (p', stack))
 	
   (* constants, axioms
    * the first pattern is CRUCIAL, n=0 happens very often:
@@ -380,9 +379,9 @@ and cbv_stack_value info env = function
                     cbv_stack_term info stk env br.(n-1)
 
     (* constructor in a Projection -> IOTA *)
-    | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
+    | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk)))
         when red_set (info_flags info.infos) fMATCH && Projection.unfolded p ->
-      let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
+      let arg = args.(Projection.npars p + Projection.arg p) in
 	cbv_stack_value info env (strip_appl arg stk)
 
     (* may be reduced later by application *)
@@ -407,7 +406,7 @@ let rec apply_stack info t = function
         (mkCase (ci, cbv_norm_term info env ty, t,
 		    Array.map (cbv_norm_term info env) br))
         st
-  | PROJ (p, pinfo, st) ->
+  | PROJ (p, st) ->
        apply_stack info (mkProj (p, t)) st
 
 (* performs the reduction on a constr, and returns a constr *)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index cdaa39c53c..83844c95a7 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -41,7 +41,7 @@ and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
   | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
-  | PROJ of Projection.t * Declarations.projection_body * cbv_stack
+  | PROJ of Projection.t * cbv_stack
 
 val shift_value : int -> cbv_value -> cbv_value
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 7dbef01c22..7ac08e755e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -31,7 +31,7 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of Constant.t
   | CL_IND of inductive
-  | CL_PROJ of Constant.t
+  | CL_PROJ of Projection.Repr.t
 
 type cl_info_typ = {
   cl_param : int
@@ -47,7 +47,7 @@ type coe_info_typ = {
   coe_local : bool;
   coe_context : Univ.ContextSet.t;
   coe_is_identity : bool;
-  coe_is_projection : bool;
+  coe_is_projection : Projection.Repr.t option;
   coe_param : int }
 
 let coe_info_typ_equal c1 c2 =
@@ -62,7 +62,7 @@ let coe_info_typ_equal c1 c2 =
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
   | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
   | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
   | _ -> Pervasives.compare t1 t2 (** OK *)
 
@@ -199,7 +199,7 @@ let find_class_type sigma t =
     | Var id -> CL_SECVAR id, EInstance.empty, args
     | Const (sp,u) -> CL_CONST sp, u, args
     | Proj (p, c) when not (Projection.unfolded p) ->
-      CL_PROJ (Projection.constant p), EInstance.empty, (c :: args)
+      CL_PROJ (Projection.repr p), EInstance.empty, (c :: args)
     | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
     | Prod (_,_,_) -> CL_FUN, EInstance.empty, []
     | Sort _ -> CL_SORT, EInstance.empty, []
@@ -211,7 +211,7 @@ let subst_cl_typ subst ct = match ct with
   | CL_FUN
   | CL_SECVAR _ -> ct
   | CL_PROJ c ->
-    let c',t = subst_con_kn subst c in
+    let c' = subst_proj_repr subst c in
       if c' == c then ct else CL_PROJ c'
   | CL_CONST c ->
       let c',t = subst_con_kn subst c in
@@ -248,8 +248,11 @@ let class_args_of env sigma c = pi3 (find_class_type sigma c)
 let string_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp | CL_PROJ sp ->
-      string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+  | CL_CONST sp ->
+    string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+  | CL_PROJ sp ->
+    let sp = Projection.Repr.constant sp in
+    string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
   | CL_IND sp ->
       string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp))
   | CL_SECVAR sp ->
@@ -395,7 +398,7 @@ type coercion = {
   coercion_type   : coe_typ;
   coercion_local  : bool;
   coercion_is_id  : bool;
-  coercion_is_proj  : bool;
+  coercion_is_proj  : Projection.Repr.t option;
   coercion_source : cl_typ;
   coercion_target : cl_typ;
   coercion_params : int;
@@ -408,9 +411,8 @@ let reference_arity_length ref =
   List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
 
 let projection_arity_length p =
-  let len = reference_arity_length (ConstRef p) in
-  let pb = Environ.lookup_projection (Projection.make p false) (Global.env ()) in 
-    len - pb.Declarations.proj_npars
+  let len = reference_arity_length (ConstRef (Projection.Repr.constant p)) in
+  len - Projection.Repr.npars p
 
 let class_params = function
   | CL_FUN | CL_SORT -> 0
@@ -466,13 +468,17 @@ let subst_coercion (subst, c) =
   let coe = subst_coe_typ subst c.coercion_type in
   let cls = subst_cl_typ subst c.coercion_source in
   let clt = subst_cl_typ subst c.coercion_target in
-  if c.coercion_type == coe && c.coercion_source == cls && c.coercion_target == clt then c
-  else { c with coercion_type = coe; coercion_source = cls; coercion_target = clt }
+  let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
+  if c.coercion_type == coe && c.coercion_source == cls &&
+     c.coercion_target == clt && c.coercion_is_proj == clp
+  then c
+  else { c with coercion_type = coe; coercion_source = cls;
+                coercion_target = clt; coercion_is_proj = clp; }
 
 let discharge_cl = function
   | CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
   | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
-  | CL_PROJ p -> CL_PROJ (Lib.discharge_con p)
+  | CL_PROJ p -> CL_PROJ (Lib.discharge_proj_repr p)
   | cl -> cl
 
 let discharge_coercion (_, c) =
@@ -489,6 +495,7 @@ let discharge_coercion (_, c) =
       coercion_source = discharge_cl c.coercion_source;
       coercion_target = discharge_cl c.coercion_target;
       coercion_params = n + c.coercion_params;
+      coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
     } in
     Some nc
 
@@ -509,8 +516,8 @@ let inCoercion : coercion -> obj =
 let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
   let isproj = 
     match coef with
-    | ConstRef c -> Environ.is_projection c (Global.env ())
-    | _ -> false
+    | ConstRef c -> Recordops.find_primitive_projection c
+    | _ -> None
   in
   let c = {
     coercion_type = coef;
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 35691ea37a..8df085e15c 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -21,7 +21,7 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of Constant.t
   | CL_IND of inductive
-  | CL_PROJ of Constant.t
+  | CL_PROJ of Projection.Repr.t
 
 (** Equality over [cl_typ] *)
 val cl_typ_eq : cl_typ -> cl_typ -> bool
@@ -79,7 +79,7 @@ val declare_coercion :
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
 
-val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_universe_context_set
+val coercion_value : coe_index -> (unsafe_judgment * bool * Projection.Repr.t option) Univ.in_universe_context_set
 
 (** {6 Lookup functions for coercion paths } *)
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 7be05ea600..c6c2f57dd4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -52,17 +52,17 @@ exception NoCoercionNoUnifier of evar_map * unification_error
 let apply_coercion_args env sigma check isproj argl funj =
   let rec apply_rec sigma acc typ = function
     | [] ->
-      if isproj then
-        let cst = fst (destConst sigma (j_val funj)) in
-	let p = Projection.make cst false in
-	let pb = lookup_projection p env in
-	let args = List.skipn pb.Declarations.proj_npars argl in
-	let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
-        sigma, { uj_val = applist (mkProj (p, hd), tl);
-                 uj_type = typ }
-      else
-        sigma, { uj_val = applist (j_val funj,argl);
-                 uj_type = typ }
+      (match isproj with
+       | Some p ->
+         let npars = Projection.Repr.npars p in
+         let p = Projection.make p false in
+         let args = List.skipn npars argl in
+         let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
+         sigma, { uj_val = applist (mkProj (p, hd), tl);
+                  uj_type = typ }
+       | None ->
+         sigma, { uj_val = applist (j_val funj,argl);
+                  uj_type = typ })
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
       match EConstr.kind sigma (whd_all env sigma typ) with
       | Prod (_,c1,c2) ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d0de2f8c0c..6a9a042f57 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -689,10 +689,9 @@ and detype_r d flags avoid env sigma t =
 	  (** Print the compatibility match version *)
 	  let c' = 
 	    try 
-	      let pb = Environ.lookup_projection p (snd env) in
-              let ind = pb.Declarations.proj_ind in
+              let ind = Projection.inductive p in
               let bodies = Inductiveops.legacy_match_projection (snd env) ind in
-              let body = bodies.(pb.Declarations.proj_arg) in
+              let body = bodies.(Projection.arg p) 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
@@ -1032,11 +1031,9 @@ let rec subst_glob_constr subst = DAst.map (function
       if r1' == r1 && k' == k then raw else GCast (r1',k')
 
   | GProj (p,c) as raw ->
-    let kn = Projection.constant p in
-    let b = Projection.unfolded p in
-    let kn' = subst_constant subst kn in
+    let p' = subst_proj subst p in
     let c' = subst_glob_constr subst c in
-    if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c')
+    if p' == p && c' == c then raw else GProj(p', c')
   )
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a71ef65081..984fa92c0e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -71,7 +71,7 @@ let coq_unit_judge =
 let unfold_projection env evd ts p c =
   let cst = Projection.constant p in
     if is_transparent_constant ts cst then
-      Some (mkProj (Projection.make cst true, c))
+      Some (mkProj (Projection.unfold p, c))
     else None
       
 let eval_flexible_term ts env evd c =
@@ -292,8 +292,8 @@ let ise_stack2 no_app env evd f sk1 sk2 =
 	| Success i'' -> ise_stack2 true i'' q1 q2
         | UnifFailure _ as x -> fail x)
       | UnifFailure _ as x -> fail x)
-    | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
-       if Constant.equal (Projection.constant p1) (Projection.constant p2)
+    | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 ->
+       if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
        then ise_stack2 true i q1 q2
        else fail (UnifFailure (i, NotSameHead))
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
@@ -334,8 +334,8 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 	  (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
 	  (fun i -> ise_stack2 i a1 a2)]
       else UnifFailure (i,NotSameHead)
-    | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
-       if Constant.equal (Projection.constant p1) (Projection.constant p2)
+    | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 ->
+       if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
     | Stack.App _ :: _, Stack.App _ :: _ ->
@@ -986,10 +986,9 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   let open Declarations in
   let mib = lookup_mind (fst ind) env in
-    match mib.Declarations.mind_record with
-    | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite ->
-      let (_, projs, _) = info.(snd ind) in
-      let pars = mib.Declarations.mind_nparams in
+    match get_projections env ind with
+    | Some projs when mib.mind_finite == BiFinite ->
+      let pars = mib.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
 	   let l2' = 
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 18fc08d61a..7d9debce34 100644
--- a/pretyping/heads.ml
+++ b/pretyping/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 (Environ.is_projection cst env) && is_Def cb.Declarations.const_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
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 551cc67b60..dc900ab814 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -79,7 +79,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in
   let indf = make_ind_family(pind, Context.Rel.to_extended_list mkRel 0 lnamespar) in
   let constrs = get_constructors env indf in
-  let projs = get_projections env indf in
+  let projs = get_projections env ind in
 
   let () = if Option.is_empty projs then check_privacy_block mib in
   let () = 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5760733442..b379cdf410 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -51,7 +51,7 @@ let arities_of_constructors env (ind,u as indu) =
 type inductive_family = pinductive * constr list
 
 let make_ind_family (mis, params) = (mis,params)
-let dest_ind_family (mis,params) = (mis,params)
+let dest_ind_family (mis,params) : inductive_family = (mis,params)
 
 let map_ind_family f (mis,params) = (mis, List.map f params)
 
@@ -269,11 +269,9 @@ let allowed_sorts env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_kelim
 
-let projection_nparams_env env p = 
-  let pb = lookup_projection p env in
-    pb.proj_npars
+let projection_nparams_env _ p = Projection.npars p
 
-let projection_nparams p = projection_nparams_env (Global.env ()) p
+let projection_nparams p = Projection.npars p
 
 let has_dependent_elim mib =
   match mib.mind_record with
@@ -343,17 +341,11 @@ let get_constructors env (ind,params) =
   Array.init (Array.length mip.mind_consnames)
     (fun j -> get_constructor (ind,mib,mip,params) (j+1))
 
-let get_projections env (ind,params) =
-  let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
-    match mib.mind_record with
-    | PrimRecord infos ->
-      let (_, projs, _) = infos.(snd (fst ind)) in
-      Some projs
-    | NotRecord | FakeRecord -> None
+let get_projections = Environ.get_projections
 
 let make_case_or_project env sigma indf ci pred c branches =
   let open EConstr in
-  let projs = get_projections env indf in
+  let projs = get_projections env (fst (fst indf)) in
   match projs with
   | None -> (mkCase (ci, pred, c, branches))
   | Some ps ->
@@ -481,7 +473,6 @@ let compute_projections env (kn, i as ind) =
   let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
   let rctx, _ = decompose_prod_assum (substl subst 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. *)
@@ -512,7 +503,7 @@ let compute_projections env (kn, i as ind) =
     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) =
+  let projections decl (proj_arg, j, pbs, subst) =
     match decl with
     | LocalDef (na,c,t) ->
         (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
@@ -525,11 +516,12 @@ let compute_projections env (kn, i as ind) =
            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)
+        (proj_arg, 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
+        let lab = Label.of_id id in
+        let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab 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
@@ -544,12 +536,12 @@ let compute_projections env (kn, i as ind) =
         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)
+        (proj_arg + 1, 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, [], [])
+  let (_, _, pbs, subst) =
+    List.fold_right projections ctx (0, 1, [], [])
   in
   Array.rev_of_list pbs
 
@@ -738,8 +730,8 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
       !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
 
 let type_of_projection_constant env (p,u) =
-  let pb = lookup_projection p env in
-  Vars.subst_instance_constr u pb.proj_type
+  let pty = lookup_projection p env in
+  Vars.subst_instance_constr u pty
 
 let type_of_projection_knowing_arg env sigma p c ty =
   let c = EConstr.Unsafe.to_constr c in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 8eaef24c48..ea34707bfc 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -130,7 +130,10 @@ val has_dependent_elim : mutual_inductive_body -> bool
 
 (** Primitive projections *)
 val projection_nparams : Projection.t -> int
+[@@ocaml.deprecated "Use [Projection.npars]"]
 val projection_nparams_env : env -> Projection.t -> int
+[@@ocaml.deprecated "Use [Projection.npars]"]
+
 val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
 				     EConstr.t -> EConstr.types -> types
 
@@ -149,7 +152,8 @@ val get_constructor :
   pinductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
 val get_constructors : env -> inductive_family -> constructor_summary array
-val get_projections  : env -> inductive_family -> Constant.t array option
+val get_projections  : env -> inductive -> Projection.Repr.t array option
+[@@ocaml.deprecated "Use [Environ.get_projections]"]
 
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 21c2022057..5df41ef76a 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -185,14 +185,13 @@ let branch_of_switch lvl ans bs =
     bs ci in
   Array.init (Array.length tbl) branch
 
-let get_proj env ((mind, n), i) =
-  let mib = Environ.lookup_mind mind env in
-  match mib.mind_record with
-  | NotRecord | FakeRecord ->
+let get_proj env (ind, proj_arg) =
+  let mib = Environ.lookup_mind (fst ind) env in
+  match Declareops.inductive_make_projection ind mib ~proj_arg with
+  | None ->
     CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
-  | PrimRecord info ->
-    let _, projs, _ = info.(n) in
-    Projection.make projs.(i) true
+  | Some p ->
+    Projection.make p true
 
 let rec nf_val env sigma v typ =
   match kind_of_value v with
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 685aa400b8..f7fea22c0f 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -287,8 +287,7 @@ let rec subst_pattern subst pat =
   | PEvar _
   | PRel _ -> pat
   | PProj (p,c) -> 
-      let p' = Projection.map (fun p -> 
-	destConstRef (fst (subst_global subst (ConstRef p)))) p in
+      let p' = Projection.map (subst_mind subst) p in
       let c' = subst_pattern subst c in
 	if p' == p && c' == c then pat else
 	  PProj(p',c')
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 122979c1a0..3b9a8e6a1d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -773,11 +773,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     in
     let app_f = 
       match EConstr.kind !evdref fj.uj_val with
-      | Const (p, u) when Environ.is_projection p env.ExtraEnv.env ->
+      | Const (p, u) when Recordops.is_primitive_projection p ->
+        let p = Option.get @@ Recordops.find_primitive_projection p in
 	let p = Projection.make p false in
-	let pb = Environ.lookup_projection p env.ExtraEnv.env in
-	let npars = pb.Declarations.proj_npars in
-	  fun n -> 
+        let npars = Projection.npars p in
+          fun n ->
 	    if n == npars + 1 then fun _ v -> mkProj (p, v)
 	    else fun f v -> applist (f, [v])
       | _ -> fun _ f v -> applist (f, [v])
@@ -905,6 +905,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let cloc = loc_of_glob_constr c in
 	  error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj
     in
+    let ind = fst (fst (dest_ind_family indf)) in
     let cstrs = get_constructors env.ExtraEnv.env indf in
     if not (Int.equal (Array.length cstrs) 1) then
       user_err ?loc  (str "Destructing let is only for inductive types" ++
@@ -915,7 +916,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
       let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in
-      match get_projections env.ExtraEnv.env indf with
+      match Environ.get_projections env.ExtraEnv.env ind with
       | None ->
 	 List.map2 set_name (List.rev nal) cs.cs_args, false
       | Some ps ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 56a8830991..2f861c117b 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -44,7 +44,7 @@ type struc_typ = {
 let structure_table =
   Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
 let projection_table =
-  Summary.ref Cmap.empty ~name:"record-projs"
+  Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs"
 
 (* TODO: could be unify struc_typ and struc_tuple ? in particular,
    is the inductive always (fst constructor) ? It seems so... *)
@@ -53,7 +53,9 @@ type struc_tuple =
     inductive * constructor * (Name.t * bool) list * Constant.t option list
 
 let load_structure i (_,(ind,id,kl,projs)) =
-  let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+  let open Declarations in
+  let mib, mip = Global.lookup_inductive ind in
+  let n = mib.mind_nparams in
   let struc =
     { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
   structure_table := Indmap.add ind struc !structure_table;
@@ -107,6 +109,34 @@ let find_projection = function
   | ConstRef cst -> Cmap.find cst !projection_table
   | _ -> raise Not_found
 
+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 cache_prim p = load_prim 1 p
+
+let subst_prim (subst,p) = subst_proj_repr subst p
+
+let discharge_prim (_,p) = Some (Lib.discharge_proj_repr p)
+
+let inPrim : Projection.Repr.t -> obj =
+  declare_object {
+    (default_object "PRIMPROJS") with
+    cache_function = cache_prim ;
+    load_function = load_prim;
+    subst_function = subst_prim;
+    classify_function = (fun x -> Substitute x);
+    discharge_function = discharge_prim }
+
+let declare_primitive_projection p = Lib.add_anonymous_leaf (inPrim p)
+
+let is_primitive_projection c = Cmap_env.mem c !prim_table
+
+let find_primitive_projection c =
+  try Some (Cmap_env.find c !prim_table) with Not_found -> None
+
 (************************************************************************)
 (*s A canonical structure declares "canonical" conversion hints between *)
 (*  the effective components of a structure and the projections of the  *)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 748f053b2f..415b964168 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -44,6 +44,13 @@ val find_projection_nparams : GlobRef.t -> int
 (** raise [Not_found] if not a projection *)
 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 is_primitive_projection : Constant.t -> bool
+
+val find_primitive_projection : Constant.t -> Projection.Repr.t option
+
 (** {6 Canonical structures } *)
 (** A canonical structure declares "canonical" conversion hints between 
     the effective components of a structure and the projections of the  
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7fb1a0a578..63c7ab3c69 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -280,7 +280,7 @@ sig
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * Projection.t * Cst_stack.t
+  | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
   and 'a t = 'a member list
@@ -337,7 +337,7 @@ struct
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * Projection.t * Cst_stack.t
+  | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
   and 'a t = 'a member list
@@ -351,9 +351,8 @@ struct
        str "ZCase(" ++
 	 prvect_with_sep (pr_bar) pr_c br
        ++ str ")"
-    | Proj (n,m,p,cst) ->
-      str "ZProj(" ++ int n ++ pr_comma () ++ int m ++
-	pr_comma () ++ Constant.print (Projection.constant p) ++ str ")"
+    | Proj (p,cst) ->
+      str "ZProj(" ++ Constant.print (Projection.constant p) ++ str ")"
     | Fix (f,args,cst) ->
        str "ZFix(" ++ Termops.pr_fix pr_c f
        ++ pr_comma () ++ pr pr_c args ++ str ")"
@@ -413,10 +412,9 @@ struct
         (f t1 t2) && (equal_rec s1' s2')
       | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 ->
         f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
-      | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) ->
-         Int.equal n1 n2 && Int.equal m1 m2
-           && Constant.equal (Projection.constant p) (Projection.constant p2)
-           && equal_rec s1 s2
+      | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
+        Projection.Repr.equal (Projection.repr p) (Projection.repr p2)
+        && equal_rec s1 s2
       | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
         f_fix f1 f2
           && equal_rec (List.rev s1) (List.rev s2)
@@ -436,7 +434,7 @@ struct
       | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2
       | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
-      | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) ->
+      | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
 	Int.equal bal 0 && compare_rec 0 s1 s2
       | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -456,7 +454,7 @@ struct
         aux (f o t1 t2) l1 l2
       | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 ->
         aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
-      | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 ->
+      | Proj (p1,_) :: q1, Proj (p2,_) :: q2 ->
         aux o q1 q2
       | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 ->
         let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in
@@ -469,7 +467,7 @@ struct
     in aux o (List.rev sk1) (List.rev sk2)
 
   let rec map f x = List.map (function
-                               | (Proj (_,_,_,_)) as e -> e
+                               | (Proj (_,_)) as e -> e
 			       | App (i,a,j) ->
 				  let le = j - i + 1 in
 				  App (0,Array.map f (Array.sub a i le), le-1)
@@ -513,7 +511,7 @@ struct
   let will_expose_iota args =
     List.exists
       (function (Fix (_,_,l) | Case (_,_,_,l) |
-		 Proj (_,_,_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false)
+                 Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false)
       args
 
   let list_of_app_stack s =
@@ -590,9 +588,9 @@ struct
     zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
   | f, (Cst (cst,_,_,params,_)::s) ->
     zip (constr_of_cst_member cst (params @ (append_app [|f|] s)))
-  | f, (Proj (n,m,p,cst_l)::s) when refold ->
+  | f, (Proj (p,cst_l)::s) when refold ->
     zip (best_state sigma (mkProj (p,f),s) cst_l)
-  | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s)
+  | f, (Proj (p,_)::s) -> zip (mkProj (p,f),s)
   in
   zip s
 
@@ -920,16 +918,13 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 			(arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
        ) else fold ()
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
-      (let pb = lookup_projection p env in
-       let kn = Projection.constant p in
-       let npars = pb.Declarations.proj_npars 
-       and arg = pb.Declarations.proj_arg in
-	 if not tactic_mode then 
-	   let stack' = (c, Stack.Proj (npars, arg, p, Cst_stack.empty (*cst_l*)) :: stack) in
+      (let npars = Projection.npars p in
+         if not tactic_mode then
+           let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
 	     whrec Cst_stack.empty stack'
-	 else match ReductionBehaviour.get (Globnames.ConstRef kn) with
+         else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with
 	 | None ->
-	   let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in
+           let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
 	   let stack'', csts = whrec Cst_stack.empty stack' in
 	     if equal_stacks sigma stack' stack'' then fold ()
 	     else stack'', csts
@@ -946,7 +941,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	       |[] -> (* if nargs has been specified *)
 		(* CAUTION : the constant is NEVER refold
                    (even when it hides a (co)fix) *)
-		 let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in
+                 let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
 		   whrec Cst_stack.empty(* cst_l *) stack'
 	       | curr::remains -> 
 		 if curr == 0 then (* Try to reduce the record argument *)
@@ -1005,8 +1000,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
 	  whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
-	|args, (Stack.Proj (n,m,p,_)::s') when use_match ->
-	  whrec Cst_stack.empty (Stack.nth args (n+m), s')
+        |args, (Stack.Proj (p,_)::s') when use_match ->
+          whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s')
 	|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
 	  let x' = Stack.zip sigma (x, args) in
 	  let out_sk = s' @ (Stack.append_app [|x'|] s'') in
@@ -1025,14 +1020,11 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 		whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
 		  (body, s' @ (Stack.append_app [|x'|] s'')))
 	    | Stack.Cst_proj p ->
-	      let pb = lookup_projection p env in
-	      let npars = pb.Declarations.proj_npars in
-	      let narg = pb.Declarations.proj_arg in
-	      let stack = s' @ (Stack.append_app [|x'|] s'') in
+              let stack = s' @ (Stack.append_app [|x'|] s'') in
 		match Stack.strip_n_app 0 stack with
 		| None -> assert false
 		| Some (_,arg,s'') ->
-		  whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,p,cst_l) :: s''))
+                  whrec Cst_stack.empty (arg, Stack.Proj (p,cst_l) :: s''))
 	  | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with
 	    | None -> fold ()
 	    | Some (bef,arg,s''') ->
@@ -1090,10 +1082,7 @@ let local_whd_state_gen flags sigma =
       | _ -> s)
 
     | Proj (p,c) when CClosure.RedFlags.red_projection flags p ->
-      (let pb = lookup_projection p (Global.env ()) in
-	 whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
-			       p, Cst_stack.empty)
-           :: stack))
+      (whrec (c, Stack.Proj (p, Cst_stack.empty) :: stack))
 
     | Case (ci,p,d,lf) ->
       whrec (d, Stack.Case (ci,p,lf,Cst_stack.empty) :: stack)
@@ -1116,8 +1105,8 @@ let local_whd_state_gen flags sigma =
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
 	  whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
-	|args, (Stack.Proj (n,m,p,_) :: s') when use_match ->
-	  whrec (Stack.nth args (n+m), s')
+        |args, (Stack.Proj (p,_) :: s') when use_match ->
+          whrec (Stack.nth args (Projection.npars p + Projection.arg p), s')
 	|args, (Stack.Fix (f,s',cst)::s'') when use_fix ->
 	  let x' = Stack.zip sigma (x,args) in
 	  whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s''))
@@ -1576,11 +1565,11 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
 	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
 	if isConstruct sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
-      |args, (Stack.Proj (n,m,p,_) :: stack'') ->
+      |args, (Stack.Proj (p,_) :: stack'') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
 	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
 	if isConstruct sigma t_o then
-	  whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
+          whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'')
 	else s,csts'
       |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts'
   in whrec csts s
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 9256fa7ce6..b44c642d43 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -75,7 +75,7 @@ module Stack : sig
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * Projection.t * Cst_stack.t
+  | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
     * 'a t * Cst_stack.t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 869d14c627..599a0f8162 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -597,12 +597,11 @@ let recargs = function
   | EvalVar _ | EvalRel _ | EvalEvar _ -> None
   | EvalConst c -> ReductionBehaviour.get (ConstRef c)
 
-let reduce_projection env sigma pb (recarg'hd,stack') stack =
+let reduce_projection env sigma p ~npars (recarg'hd,stack') stack =
   (match EConstr.kind sigma recarg'hd with
   | Construct _ -> 
-    let proj_narg = 
-      pb.Declarations.proj_npars + pb.Declarations.proj_arg
-    in Reduced (List.nth stack' proj_narg, stack)
+    let proj_narg = npars + Projection.arg p in
+    Reduced (List.nth stack' proj_narg, stack)
   | _ -> NotReducible)
 
 let reduce_proj env sigma whfun whfun' c =
@@ -613,10 +612,8 @@ let reduce_proj env sigma whfun whfun' c =
       let constr, cargs = whfun c' in
 	(match EConstr.kind sigma constr with
 	| Construct _ -> 
-	  let proj_narg = 
-	    let pb = lookup_projection proj env in
-	      pb.Declarations.proj_npars + pb.Declarations.proj_arg
-	  in List.nth cargs proj_narg
+          let proj_narg = Projection.npars proj + Projection.arg proj in
+          List.nth cargs proj_narg
 	| _ -> raise Redelimination)
     | Case (n,p,c,brs) -> 
       let c' = redrec c in
@@ -765,22 +762,22 @@ and whd_simpl_stack env sigma =
         (try 
 	   let unf = Projection.unfolded p in
 	     if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
-	       let pb = lookup_projection p env in
+               let npars = Projection.npars p in
  		 (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with
  		 | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f -> 
                    (* simpl never *) s'
 		 | false, Some (l, n, f) when not (List.is_empty l) ->
 		   let l' = List.map_filter (fun i -> 
-		     let idx = (i - (pb.Declarations.proj_npars + 1)) in
+                     let idx = (i - (npars + 1)) in
 		       if idx < 0 then None else Some idx) l in
 		   let stack = reduce_params env sigma stack l' in
-		     (match reduce_projection env sigma pb 
+                     (match reduce_projection env sigma p ~npars
 		       (whd_construct_stack env sigma c) stack 
 		      with
 		      | Reduced s' -> redrec (applist s')
 		      | NotReducible -> s')
  		 | _ ->
-		   match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with
+                   match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with
 		   | Reduced s' -> redrec (applist s')
 		   | NotReducible -> s')
 	   else s'
@@ -852,8 +849,8 @@ let try_red_product env sigma c =
 	  | Construct _ -> c
 	  | _ -> redrec env c
 	in
-	let pb = lookup_projection p env in
-          (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with
+        let npars = Projection.npars p in
+          (match reduce_projection env sigma p ~npars (whd_betaiotazeta_stack sigma c') [] with
 	  | Reduced s -> simpfun (applist s)
 	  | NotReducible -> raise Redelimination)
       | _ -> 
@@ -946,8 +943,8 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
 	  (match EConstr.kind sigma constr with
 	  | Const (c', _) -> Constant.equal (Projection.constant p) c'
 	  | _ -> false) ->
-	let pb = Environ.lookup_projection p env in
-	  if List.length stack <= pb.Declarations.proj_npars then
+        let npars = Projection.npars p in
+          if List.length stack <= npars then
 	    (** Do not show the eta-expanded form *)
 	    s'
 	  else redrec (applist (c, stack))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ca2702d741..4ba715f0d5 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -253,16 +253,16 @@ let judge_of_variable env id =
   Termops.on_judgment EConstr.of_constr (judge_of_variable env id)
 
 let judge_of_projection env sigma p cj =
-  let pb = lookup_projection p env in
+  let pty = lookup_projection p env in
   let (ind,u), args =
     try find_mrectype env sigma cj.uj_type
     with Not_found -> error_case_not_inductive env sigma cj
   in
   let u = EInstance.kind sigma u in
-    let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in
-    let ty = substl (cj.uj_val :: List.rev args) ty in
-      {uj_val = EConstr.mkProj (p,cj.uj_val);
-       uj_type = ty}
+  let ty = EConstr.of_constr (CVars.subst_instance_constr u pty) in
+  let ty = substl (cj.uj_val :: List.rev args) ty in
+  {uj_val = EConstr.mkProj (p,cj.uj_val);
+   uj_type = ty}
 
 let judge_of_abstraction env name var j =
   { uj_val = mkLambda (name, var.utj_val, j.uj_val);
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4ba5d27947..fc1f6fc81e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -478,12 +478,8 @@ let expand_table_key env = function
   | RelKey _ -> None
 
 let unfold_projection env p stk =
-  (match try Some (lookup_projection p env) with Not_found -> None with
-  | Some pb -> 
-    let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
-			p, Cst_stack.empty) in
-      s :: stk
-  | None -> assert false)
+  let s = Stack.Proj (p, Cst_stack.empty) in
+  s :: stk
 
 let expand_key ts env sigma = function
   | Some (IsKey k) -> Option.map EConstr.of_constr (expand_table_key env k)
@@ -512,7 +508,7 @@ let key_of env sigma b flags f =
   match EConstr.kind sigma f with
   | Const (cst, u) when is_transparent env (ConstKey cst) &&
       (Cpred.mem cst (snd flags.modulo_delta)
-       || Environ.is_projection cst env) ->
+       || Recordops.is_primitive_projection cst) ->
       let u = EInstance.kind sigma u in
       Some (IsKey (ConstKey (cst, u)))
   | Var id when is_transparent env (VarKey id) && 
@@ -669,17 +665,15 @@ let is_eta_constructor_app env sigma ts f l1 term =
   | _ -> false
 
 let eta_constructor_app env sigma f l1 term =
-  let open Declarations in
   match EConstr.kind sigma f with
   | Construct (((_, i as ind), j), u) ->
     let mib = lookup_mind (fst ind) env in
-      (match mib.Declarations.mind_record with
-      | PrimRecord info ->
-        let (_, projs, _) = info.(i) in
+      (match get_projections env ind with
+      | Some projs ->
         let npars = mib.Declarations.mind_nparams in
 	let pars, l1' = Array.chop npars l1 in
 	let arg = Array.append pars [|term|] in
-	let l2 = Array.map (fun p -> mkApp (mkConstU (p,u), arg)) projs in
+        let l2 = Array.map (fun p -> mkApp (mkConstU (Projection.Repr.constant p,u), arg)) projs in
 	  l1', l2
       | _ -> assert false)
   | _ -> assert false