Projections use index representation

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

78 files changed, 683 insertions, 484 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 4846a9af8c..df747692a4 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -202,16 +202,6 @@ type inline = int option
 (** A constant can have no body (axiom/parameter), or a
     transparent body, or an opaque one *)
 
-(** Projections are a particular kind of constant: 
-    always transparent. *)
-
-type projection_body = {
-  proj_ind : inductive;
-  proj_npars : int;
-  proj_arg : int;
-  proj_type : constr; (* Type under params *)
-}
-
 type constant_def =
   | Undef of inline
   | Def of constr_substituted
@@ -254,7 +244,7 @@ type wf_paths = recarg Rtree.t
 type record_info =
 | NotRecord
 | FakeRecord
-| PrimRecord of (Id.t * Constant.t array * projection_body array) array
+| PrimRecord of (Id.t * Label.t array * constr array) array
 
 type regular_inductive_arity = {
   mind_user_arity : constr;
diff --git a/checker/closure.ml b/checker/closure.ml
index 2dcc1a9840..5706011607 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -273,7 +273,7 @@ let update v1 (no,t) =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Projection.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -497,8 +497,8 @@ let rec zip m stk =
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
-    | Zproj (i,j,cst) :: s -> 
-        zip {norm=neutr m.norm; term=FProj (cst,m)} s
+    | Zproj p :: s ->
+        zip {norm=neutr m.norm; term=FProj (Projection.make p true,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
     | Zshift(n)::s ->
@@ -618,21 +618,25 @@ let drop_parameters depth n argstk =
 
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
-    match mib.mind_record with
-    | PrimRecord info when mib.mind_finite <> CoFinite ->
-      let (_, projs, pbs) = info.(snd ind) in
-	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
-	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
-      let pars = mib.mind_nparams in
-      let right = fapp_stack (f, s') in
-      let (depth, args, s) = strip_update_shift_app m s in
-      (** Try to drop the params, might fail on partially applied constructors. *)
-      let argss = try_drop_parameters depth pars args in
-	let hstack =
-	  Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-			     term = FProj (Projection.make p false, right) }) projs in
-	argss, [Zapp hstack]	
-    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+  (* disallow eta-exp for non-primitive records *)
+  if not (mib.mind_finite == BiFinite) then raise Not_found;
+  match Declarations.inductive_make_projections ind mib with
+  | Some projs ->
+    (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+       arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
+    let pars = mib.mind_nparams in
+    let right = fapp_stack (f, s') in
+    let (depth, args, s) = strip_update_shift_app m s in
+    (** Try to drop the params, might fail on partially applied constructors. *)
+    let argss = try_drop_parameters depth pars args in
+    let hstack =
+      Array.map (fun p ->
+          { norm = Red; (* right can't be a constructor though *)
+            term = FProj (Projection.make p false, right) })
+        projs
+    in
+    argss, [Zapp hstack]
+  | None -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
@@ -669,8 +673,7 @@ let contract_fix_vect fix =
   (subs_cons(Array.init nfix make_body, env), thisbody)
 
 let unfold_projection env p =
-  let pb = lookup_projection p env in
-  Zproj (pb.proj_npars, pb.proj_arg, p)
+  Zproj (Projection.repr p)
 
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
@@ -748,9 +751,9 @@ let rec knr info m stk =
             let stk' = par @ append_stack [|rarg|] s in
             let (fxe,fxbd) = contract_fix_vect fx.term in
             knit info fxe fxbd stk'
-       | (depth, args, Zproj (n, m, cst)::s) ->
-	    let rargs = drop_parameters depth n args in
-	    let rarg = project_nth_arg m rargs in
+       | (depth, args, Zproj p::s) ->
+            let rargs = drop_parameters depth (Projection.Repr.npars p) args in
+            let rarg = project_nth_arg (Projection.Repr.arg p) rargs in
 	    kni info rarg s
        | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
diff --git a/checker/closure.mli b/checker/closure.mli
index 49b07f730d..cec785699d 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -103,7 +103,7 @@ type fterm =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Projection.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index a744a02279..0540227ccb 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -214,11 +214,7 @@ let rec map_kn f f' c =
     match c with
       | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
       | Proj (p,t) -> 
-          let p' = 
-	    Projection.map (fun kn ->
-			    try fst (f' kn Univ.Instance.empty)
-			    with No_subst -> kn) p
-	  in
+          let p' = Projection.map f p in
 	  let t' = func t in
 	    if p' == p && t' == t then c
 	    else Proj (p', t')
@@ -495,6 +491,16 @@ let eq_recarg r1 r2 = match r1, r2 with
 
 let eq_wf_paths = Rtree.equal eq_recarg
 
+let inductive_make_projections ind mib =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    let projs = Array.mapi (fun proj_arg lab ->
+        Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab)
+        (pi2 infos.(snd ind))
+    in
+    Some projs
+
 (**********************************************************************)
 (* Representation of mutual inductive types in the kernel             *)
 (*
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 7458b3e0b0..ce852644ef 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -25,6 +25,9 @@ val dest_subterms : wf_paths -> wf_paths list array
 val eq_recarg : recarg -> recarg -> bool
 val eq_wf_paths : wf_paths -> wf_paths -> bool
 
+val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
+  Names.Projection.Repr.t array option
+
 (* Modules *)
 
 val empty_delta_resolver : delta_resolver
diff --git a/checker/environ.ml b/checker/environ.ml
index ba1eb0ddb4..74cf237763 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -7,7 +7,6 @@ open Declarations
 
 type globals = {
   env_constants : constant_body Cmap_env.t;
-  env_projections : projection_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
   env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
@@ -35,7 +34,6 @@ let empty_oracle = {
 let empty_env = {
   env_globals =
   { env_constants = Cmap_env.empty;
-    env_projections = Cmap_env.empty;
     env_inductives = Mindmap_env.empty;
     env_inductives_eq = KNmap.empty;
     env_modules = MPmap.empty;
@@ -166,9 +164,6 @@ let evaluable_constant cst env =
   try let _  = constant_value env (cst, Univ.Instance.empty) in true
   with Not_found | NotEvaluableConst _ -> false
 
-let lookup_projection p env =
-  Cmap_env.find (Projection.constant p) env.env_globals.env_projections
-
 (* Mutual Inductives *)
 let scrape_mind env kn=
   try
@@ -191,14 +186,6 @@ let add_mind kn mib env =
     Printf.ksprintf anomaly ("Inductive %s is already defined.")
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
-  let new_projections = match mib.mind_record with
-    | NotRecord | FakeRecord -> env.env_globals.env_projections
-    | PrimRecord projs ->
-      Array.fold_left (fun accu (id, kns, pbs) ->
-      Array.fold_left2 (fun accu kn pb ->
-          Cmap_env.add kn pb accu) accu kns pbs)
-        env.env_globals.env_projections projs
-  in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
   let new_inds_eq = if KerName.equal kn1 kn2 then
     env.env_globals.env_inductives_eq
@@ -207,10 +194,22 @@ let add_mind kn mib env =
   let new_globals =
     { env.env_globals with
       env_inductives = new_inds;
-      env_projections = new_projections;
       env_inductives_eq = new_inds_eq} in
   { env with env_globals = new_globals }
 
+let lookup_projection p env =
+  let mind,i = Projection.inductive p in
+  let mib = lookup_mind mind env in
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> CErrors.anomaly ~label:"lookup_projection" Pp.(str "not a projection")
+  | PrimRecord infos ->
+    let _,labs,typs = infos.(i) in
+    let parg = Projection.arg p in
+    if not (Label.equal labs.(parg) (Projection.label p))
+    then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect label on projection")
+    else if not (Int.equal mib.mind_nparams (Projection.npars p))
+    then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect param number on projection")
+    else typs.(parg)
 
 (* Modules *)
 
diff --git a/checker/environ.mli b/checker/environ.mli
index acb29d7d2d..af1b2a6228 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -5,7 +5,6 @@ open Cic
 
 type globals = {
   env_constants : constant_body Cmap_env.t;
-  env_projections : projection_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
   env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
@@ -58,7 +57,8 @@ exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> Constant.t puniverses -> constr
 val evaluable_constant : Constant.t -> env -> bool
 
-val lookup_projection : Projection.t -> env -> projection_body
+(** NB: here in the checker we check the inferred info (npars, label) *)
+val lookup_projection : Projection.t -> env -> constr
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 16c7012138..ae15a36d57 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -43,7 +43,7 @@ let compare_stack_shape stk1 stk2 =
     | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
     | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
-    | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
+    | (Zproj p1::s1, Zproj p2::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
     | ((ZcaseT(c1,_,_,_))::s1,
        (ZcaseT(c2,_,_,_))::s2) ->
@@ -55,7 +55,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.Projection.t * lift
+  | Zlproj of Names.Projection.Repr.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -74,8 +74,8 @@ let pure_stack lfts stk =
             | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
             | (Zapp a, (l,pstk)) ->
                 (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
-	    | (Zproj (n,m,c), (l,pstk)) ->
-		(l, Zlproj (c,l)::pstk)
+            | (Zproj p, (l,pstk)) ->
+                (l, Zlproj (p,l)::pstk)
             | (Zfix(fx,a),(l,pstk)) ->
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
@@ -143,9 +143,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 f fx1 fx2; cmp_rec a1 a2
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-               if not (Names.Constant.UserOrd.equal
-		       (Names.Projection.constant c1)
-		       (Names.Projection.constant c2)) then 
+               if not (Names.Projection.Repr.UserOrd.equal c1 c2) then
 		raise NotConvertible
             | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
@@ -257,7 +255,7 @@ let rec no_case_available = function
   | Zupdate _ :: stk -> no_case_available stk
   | Zshift _ :: stk -> no_case_available stk
   | Zapp _ :: stk -> no_case_available stk
-  | Zproj (_,_,_) :: _ -> false
+  | Zproj _ :: _ -> false
   | ZcaseT _ :: _ -> false
   | Zfix _ :: _ -> true
 
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 3f7f844704..0916d98ddf 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -12,7 +12,6 @@
 open Util
 open Names
 open Cic
-open Term
 open Declarations
 open Environ
 open Reduction
@@ -123,14 +122,6 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       env, Univ.make_abstract_instance auctx'
     | _ -> error ()
   in
-  let eq_projection_body p1 p2 =
-    let check eq f = if not (eq (f p1) (f p2)) then error () in
-    check eq_ind (fun x -> x.proj_ind);
-    check (==) (fun x -> x.proj_npars);
-    check (==) (fun x -> x.proj_arg);
-    check (eq_constr) (fun x -> x.proj_type);
-    true
-  in
   let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in
 
   let check_packet p1 p2 =
@@ -188,9 +179,9 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     | FakeRecord, FakeRecord -> true
     | PrimRecord info1, PrimRecord info2 ->
       let check (id1, p1, pb1) (id2, p2, pb2) =
-        Id.equal id1 id2 &&
-        Array.for_all2 Constant.UserOrd.equal p1 p2 &&
-        Array.for_all2 eq_projection_body pb1 pb2
+        (* we don't care about the id, the types are inferred from the inductive
+           (ie checked before now) *)
+        Array.for_all2 Label.equal p1 p2
       in
       Array.equal check info1 info2
     | _, _ -> false
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 19ede4b9a2..138fe8bc95 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -198,14 +198,13 @@ let judge_of_case env ci pj (c,cj) lfj =
 (* Projection. *)
 
 let judge_of_projection env p c ct =
-  let pb = lookup_projection p env in
+  let pty = lookup_projection p env in
   let (ind,u), args =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (c, ct)
   in
-    assert(eq_ind pb.proj_ind ind);
-    let ty = subst_instance_constr u pb.proj_type in
-      substl (c :: List.rev args) ty
+  let ty = subst_instance_constr u pty in
+  substl (c :: List.rev args) ty
 
 (* Fixpoints. *)
 
diff --git a/checker/values.ml b/checker/values.ml
index 88cdb644db..e68cd18b87 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 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli
+MD5 064cd8d9651d37aebf77fb638b889cad checker/cic.mli
 
 *)
 
@@ -135,7 +135,9 @@ let v_caseinfo =
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 4
-let v_proj = v_tuple "projection" [|v_cst; v_bool|]
+
+let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|]
+let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
 
 let rec v_constr =
   Sum ("constr",0,[|
@@ -223,10 +225,6 @@ let v_cst_def =
   v_sum "constant_def" 0
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
-let v_projbody =
-  v_tuple "projection_body"
-    [|v_ind;Int;Int;v_constr|]
-
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
 
@@ -277,7 +275,7 @@ let v_finite = v_enum "recursivity_kind" 3
 
 let v_record_info =
   v_sum "record_info" 2
-    [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |]
+    [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
 
 let v_ind_pack_univs = 
   v_sum "abstract_inductive_universes" 0
diff --git a/clib/cArray.ml b/clib/cArray.ml
index fc87a74cf6..d509c55b9a 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -59,6 +59,7 @@ sig
     ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
   val map_left : ('a -> 'b) -> 'a array -> 'b array
   val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
+  val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
   val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
   val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
   val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
@@ -407,6 +408,12 @@ let iter2 f v1 v2 =
   let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in
   for i = 0 to len1 - 1 do f (uget v1 i) (uget v2 i) done
 
+let iter2_i f v1 v2 =
+  let len1 = Array.length v1 in
+  let len2 = Array.length v2 in
+  let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in
+  for i = 0 to len1 - 1 do f i (uget v1 i) (uget v2 i) done
+
 let pure_functional = false
 
 let fold_right_map f v e =
diff --git a/clib/cArray.mli b/clib/cArray.mli
index 8bf33f82f9..5c7e09eeac 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -101,6 +101,9 @@ sig
   val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
   (** Iter on two arrays. Raise [Invalid_argument "Array.iter2"] if sizes differ. *)
 
+  val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
+  (** Iter on two arrays. Raise [Invalid_argument "Array.iter2_i"] if sizes differ. *)
+
   val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
   (** [fold_left_map f e_0 [|l_1...l_n|] = e_n,[|k_1...k_n|]]
     where [(e_i,k_i)=f e_{i-1} l_i]; see also [Smart.fold_left_map] *)
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index c8385da618..98190b05b5 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -17,7 +17,7 @@ let ppripos (ri,pos) =
   | Reloc_getglobal kn ->
     print_string ("getglob "^(Constant.to_string kn)^"\n")
   | Reloc_proj_name p ->
-    print_string ("proj "^(Constant.to_string p)^"\n")
+    print_string ("proj "^(Projection.Repr.to_string p)^"\n")
   );
    print_flush ()
 
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 005ef16351..3dc1933a14 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -565,9 +565,8 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   | App (f, args), Proj (p, c) -> 
       (match kind_upto sigma f with
       | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
-          let pb = Environ.lookup_projection p env in
-          let npars = pb.Declarations.proj_npars in
-	  if Array.length args == npars + 1 then
+          let npars = Projection.npars p in
+          if Array.length args == npars + 1 then
             eqc' 0 c args.(npars)
 	  else false
       | _ -> false)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cb50245d5a..c87768b190 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2059,6 +2059,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CProj (pr, c) ->
       match intern_reference pr with
       | ConstRef p ->
+        let p = Option.get @@ Recordops.find_primitive_projection p in
         DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
       | _ ->
         raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
diff --git a/interp/declare.ml b/interp/declare.ml
index fcb62ac8c4..0222aeb283 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -382,40 +382,44 @@ let inInductive : inductive_obj -> obj =
     discharge_function = discharge_inductive;
     rebuild_function = infer_inductive_subtyping }
 
+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 *)
+      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
+  ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent))
+
 let declare_projections univs mind =
   let env = Global.env () in
   let mib = Environ.lookup_mind mind env in
   match mib.mind_record with
   | PrimRecord info ->
-    let iter i (_, kns, _) =
-      let mind = (mind, i) in
-      let projs = Inductiveops.compute_projections env mind in
-      Array.iter2 (fun kn (term, types) ->
-	let id = Label.to_id (Constant.label kn) in
-        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
+    let iter_ind i (_, labs, _) =
+      let ind = (mind, i) in
+      let projs = Inductiveops.compute_projections env ind in
+      Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
     in
-    let () = Array.iteri iter info in
-    true, true
-  | FakeRecord -> true, false
-  | NotRecord -> false, false
+    let () = Array.iteri iter_ind info in
+    true
+  | FakeRecord -> false
+  | NotRecord -> false
 
 (* for initial declaration *)
 let declare_mind mie =
@@ -424,7 +428,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 mie.mind_entry_universes mind in
+  let isprim = declare_projections mie.mind_entry_universes mind in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   oname, isprim
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 8aa1e62504..e542b818f6 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -689,8 +689,8 @@ let check_rigidity isrigid =
     user_err  (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
 
 let projection_implicits env p impls = 
-  let pb = Environ.lookup_projection p env in
-    CList.skipn_at_least pb.Declarations.proj_npars impls
+  let npars = Projection.npars p in
+  CList.skipn_at_least npars impls
 
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ab0bf9c6fe..7cde563cd2 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -641,11 +641,9 @@ let rec subst_notation_constr subst bound raw =
       if r1' == r1 && k' == k then raw else NCast(r1',k')
 
   | NProj (p, c) ->
-    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_notation_constr subst bound c in
-    if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c')
+    if p' == p && c' == c then raw else NProj(p', c')
 
 
 let subst_interpretation subst (metas,pat) =
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 61ed40394e..ac4c6c52c6 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -397,7 +397,7 @@ let update v1 no t =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Constant.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -691,8 +691,8 @@ let rec zip m stk =
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
-    | Zproj (i,j,cst) :: s ->
-        zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s
+    | Zproj p :: s ->
+        zip {norm=neutr m.norm; term=FProj(Projection.make p true,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
     | Zshift(n)::s ->
@@ -822,21 +822,24 @@ let drop_parameters depth n argstk =
 let eta_expand_ind_stack env ind m s (f, s') =
   let open Declarations in
   let mib = lookup_mind (fst ind) env in
-    match mib.Declarations.mind_record with
-    | PrimRecord infos when
-        mib.Declarations.mind_finite == Declarations.BiFinite ->
-      let (_, projs, _) = infos.(snd ind) in
-	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+  (* disallow eta-exp for non-primitive records *)
+  if not (mib.mind_finite == BiFinite) then raise Not_found;
+  match Declareops.inductive_make_projections ind mib with
+  | Some projs ->
+    (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
-      let pars = mib.Declarations.mind_nparams in
-      let right = fapp_stack (f, s') in
-      let (depth, args, s) = strip_update_shift_app m s in
-      (** Try to drop the params, might fail on partially applied constructors. *)
-      let argss = try_drop_parameters depth pars args in
-      let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-					 term = FProj (Projection.make p true, right) }) projs in
-	argss, [Zapp hstack]
-    | PrimRecord _ | NotRecord | FakeRecord -> raise Not_found (* disallow eta-exp for non-primitive records *)
+    let pars = mib.Declarations.mind_nparams in
+    let right = fapp_stack (f, s') in
+    let (depth, args, s) = strip_update_shift_app m s in
+    (** Try to drop the params, might fail on partially applied constructors. *)
+    let argss = try_drop_parameters depth pars args in
+    let hstack = Array.map (fun p ->
+        { norm = Red; (* right can't be a constructor though *)
+          term = FProj (Projection.make p true, right) })
+        projs
+    in
+    argss, [Zapp hstack]
+  | None -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
@@ -875,9 +878,7 @@ let contract_fix_vect fix =
 let unfold_projection info p =
   if red_projection info.i_flags p
   then
-    let open Declarations in
-    let pb = lookup_projection p (info_env info) in
-    Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p))
+    Some (Zproj (Projection.repr p))
   else None
 
 (*********************************************************************)
@@ -958,9 +959,9 @@ let rec knr info tab m stk =
             let stk' = par @ append_stack [|rarg|] s in
             let (fxe,fxbd) = contract_fix_vect fx.term in
             knit info tab fxe fxbd stk'
-	| (depth, args, Zproj (n, m, cst)::s) when use_match ->
-	    let rargs = drop_parameters depth n args in
-	    let rarg = project_nth_arg m rargs in
+        | (depth, args, Zproj p::s) when use_match ->
+            let rargs = drop_parameters depth (Projection.Repr.npars p) args in
+            let rarg = project_nth_arg (Projection.Repr.arg p) rargs in
             kni info tab rarg s
         | (_,args,s) -> (m,args@s))
      else (m,stk)
@@ -1002,7 +1003,7 @@ let rec zip_term zfun m stk =
         let t = mkCase(ci, zfun (mk_clos e p), m,
 		       Array.map (fun b -> zfun (mk_clos e b)) br) in
         zip_term zfun t s
-    | Zproj(_,_,p)::s ->
+    | Zproj p::s ->
         let t = mkProj (Projection.make p true, m) in
 	zip_term zfun t s
     | Zfix(fx,par)::s ->
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index f8f98f0abe..1e3e7b48ac 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -152,7 +152,7 @@ type fterm =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Constant.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 3095ce148b..8030060339 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -128,7 +128,7 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
-  | Kproj of int * Constant.t  (* index of the projected argument,
+  | Kproj of int * Projection.Repr.t  (* index of the projected argument,
                                            name of projection *)
   | Kensurestackcapacity of int
 (* spiwack: instructions concerning integers *)
@@ -311,7 +311,7 @@ let rec pp_instr i =
 
   | Kbranch lbl -> str "branch " ++ pp_lbl lbl
 
-  | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
+  | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Projection.Repr.print p
 
   | Kensurestackcapacity size -> str "growstack " ++ int size
 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index de21401b31..9c289e87d9 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -88,7 +88,7 @@ type instruction =
   | Ksetfield of int                    (** accu[n] = sp[0] ; sp = pop sp *)
   | Kstop
   | Ksequence of bytecodes * bytecodes
-  | Kproj of int * Constant.t  (** index of the projected argument,
+  | Kproj of int * Projection.Repr.t  (** index of the projected argument,
                                             name of projection *)
   | Kensurestackcapacity of int
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2426255e48..7643fdb55f 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -27,7 +27,7 @@ type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
   | Reloc_getglobal of Names.Constant.t
-  | Reloc_proj_name of Constant.t
+  | Reloc_proj_name of Projection.Repr.t
 
 let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2
@@ -36,7 +36,7 @@ let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_const _, _ -> false
 | Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
 | Reloc_getglobal _, _ -> false
-| Reloc_proj_name p1, Reloc_proj_name p2 -> Constant.equal p1 p2
+| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2
 | Reloc_proj_name _, _ -> false
 
 let hash_reloc_info r =
@@ -45,7 +45,7 @@ let hash_reloc_info r =
   | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
   | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
   | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
-  | Reloc_proj_name p -> combinesmall 4 (Constant.hash p)
+  | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p)
 
 module RelocTable = Hashtbl.Make(struct
   type t = reloc_info
@@ -371,7 +371,7 @@ let subst_reloc s ri =
       Reloc_annot {a with ci = ci}
   | Reloc_const sc -> Reloc_const (subst_strcst s sc)
   | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
-  | Reloc_proj_name p -> Reloc_proj_name (subst_constant s p)
+  | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p)
 
 let subst_patches subst p =
   let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 696721c375..9009926bdb 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -5,7 +5,7 @@ type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
   | Reloc_getglobal of Constant.t
-  | Reloc_proj_name of Constant.t
+  | Reloc_proj_name of Projection.Repr.t
 
 type patches
 type emitcodes
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index f42c46175c..3afef339fb 100644
--- a/kernel/cinstr.mli
+++ b/kernel/cinstr.mli
@@ -36,7 +36,7 @@ and lambda =
   | Lval          of structured_constant
   | Lsort         of Sorts.t
   | Lind          of pinductive
-  | Lproj         of int * Constant.t * lambda
+  | Lproj         of int * Projection.Repr.t * lambda
   | Luint         of uint
 
 (* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index f1b6f3dffc..d2f59c432b 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -113,7 +113,7 @@ let rec pp_lam lam =
        str")")
   | Lproj(i,kn,arg) ->
     hov 1
-      (str "(proj#" ++ int i ++ spc() ++ pr_con kn ++ str "(" ++ pp_lam arg
+      (str "(proj#" ++ int i ++ spc() ++ Projection.Repr.print kn ++ str "(" ++ pp_lam arg
        ++ str ")")
   | Luint _ ->
     str "(uint)"
@@ -708,10 +708,9 @@ let rec lambda_of_constr env c =
     Lcofix(init, (names, ltypes, lbodies))
 
   | Proj (p,c) ->
-    let pb = lookup_projection p env.global_env in
-    let n = pb.proj_arg in
+    let n = Projection.arg p in
     let lc = lambda_of_constr env c in
-    Lproj (n,Projection.constant p,lc)
+    Lproj (n,Projection.repr p,lc)
 
 and lambda_of_app env f args =
   match Constr.kind f with
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 094609b963..c06358054e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -126,16 +126,13 @@ let expmod_constr cache modlist c =
 	    | Not_found -> Constr.map substrec c)
 
       | Proj (p, c') ->
-          (try
-            (** No need to expand parameters or universes for projections *)
-            let map cst =
-              let _ = Cmap.find cst (fst modlist) in
-              pop_con cst
-            in
-            let p = Projection.map map p in
-            let c' = substrec c' in
-            mkProj (p, c')
-	   with Not_found -> Constr.map substrec c)
+        let map cst npars =
+          let _, newpars = Mindmap.find cst (snd modlist) in
+          pop_mind cst, npars + Array.length newpars
+        in
+        let p' = try Projection.map_npars map p with Not_found -> p in
+        let c'' = substrec c' in
+        if p == p' && c' == c'' then c else mkProj (p', c'')
 
   | _ -> Constr.map substrec c
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index bbe0937820..bb9231d000 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -77,11 +77,7 @@ module AnnotTable = Hashtbl.Make (struct
   let hash = hash_annot_switch
 end)
 
-module ProjNameTable = Hashtbl.Make (struct
-  type t = Constant.t
-  let equal = Constant.equal
-  let hash = Constant.hash
-end)
+module ProjNameTable = Hashtbl.Make (Projection.Repr)
 
 let str_cst_tbl : int SConstTable.t = SConstTable.create 31
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 95078800e7..0811eb72fd 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -46,16 +46,6 @@ type inline = int option
 (** A constant can have no body (axiom/parameter), or a
     transparent body, or an opaque one *)
 
-(** Projections are a particular kind of constant: 
-    always transparent. *)
-
-type projection_body = {
-  proj_ind : inductive;
-  proj_npars : int;
-  proj_arg : int; (** Projection index, starting from 0 *)
-  proj_type : types; (* Type under params *)
-}
-
 (* Global declarations (i.e. constants) can be either: *)
 type constant_def =
   | Undef of inline                       (** a global assumption *)
@@ -114,7 +104,7 @@ v}
     If it is a primitive record, for every type in the block, we get:
     - The identifier for the binder name of the record in primitive projections.
     - The constants associated to each projection.
-    - The checked projection bodies.
+    - The projection types (under parameters).
 
     The kernel does not exploit the difference between [NotRecord] and
     [FakeRecord]. It is mostly used by extraction, and should be extruded from
@@ -124,7 +114,7 @@ v}
 type record_info =
 | NotRecord
 | FakeRecord
-| PrimRecord of (Id.t * Constant.t array * projection_body array) array
+| PrimRecord of (Id.t * Label.t array * types array) array
 
 type regular_inductive_arity = {
   mind_user_arity : types;
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3e6c4858e0..bbe4bc0dcb 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -83,11 +83,6 @@ let subst_const_def sub def = match def with
   | Def c -> Def (subst_constr sub c)
   | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
 
-let subst_const_proj sub pb =
-  { pb with proj_ind = subst_ind sub pb.proj_ind;
-    proj_type = subst_mps sub pb.proj_type;
-  }
-
 let subst_const_body sub cb =
   assert (List.is_empty cb.const_hyps); (* we're outside sections *)
   if is_empty_subst sub then cb
@@ -213,10 +208,9 @@ let subst_mind_record sub r = match r with
 | FakeRecord -> FakeRecord
 | PrimRecord infos ->
   let map (id, ps, pb as info) =
-    let ps' = Array.Smart.map (subst_constant sub) ps in
-    let pb' = Array.Smart.map (subst_const_proj sub) pb in
-    if ps' == ps && pb' == pb then info
-    else (id, ps', pb')
+    let pb' = Array.Smart.map (subst_mps sub) pb in
+    if pb' == pb then info
+    else (id, ps, pb')
   in
   let infos' = Array.Smart.map map infos in
   if infos' == infos then r else PrimRecord infos'
@@ -254,6 +248,25 @@ let inductive_is_cumulative mib =
   | Polymorphic_ind ctx -> false
   | Cumulative_ind cumi -> true
 
+let inductive_make_projection ind mib ~proj_arg =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    Some (Names.Projection.Repr.make ind
+            ~proj_npars:mib.mind_nparams
+            ~proj_arg
+            (pi2 infos.(snd ind)).(proj_arg))
+
+let inductive_make_projections ind mib =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    let projs = Array.mapi (fun proj_arg lab ->
+        Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab)
+        (pi2 infos.(snd ind))
+    in
+    Some projs
+
 (** {6 Hash-consing of inductive declarations } *)
 
 let hcons_regular_ind_arity a =
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index fb46112ea7..f91e69807f 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -66,6 +66,11 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool
 (** Is the inductive cumulative? *)
 val inductive_is_cumulative : mutual_inductive_body -> bool
 
+val inductive_make_projection : Names.inductive -> mutual_inductive_body -> proj_arg:int ->
+  Names.Projection.Repr.t option
+val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
+  Names.Projection.Repr.t array option
+
 (** {6 Kernel flags} *)
 
 (** A default, safe set of flags for kernel type-checking *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4ab4698031..e7efa5e2c9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -52,7 +52,6 @@ type mind_key = mutual_inductive_body * link_info ref
 
 type globals = {
   env_constants : constant_key Cmap_env.t;
-  env_projections : projection_body Cmap_env.t;
   env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t;
@@ -110,7 +109,6 @@ let empty_rel_context_val = {
 let empty_env = {
   env_globals = {
     env_constants = Cmap_env.empty;
-    env_projections = Cmap_env.empty;
     env_inductives = Mindmap_env.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
@@ -490,11 +488,24 @@ let polymorphic_pconstant (cst,u) env =
 let type_in_type_constant cst env =
   not (lookup_constant cst env).const_typing_flags.check_universes
 
-let lookup_projection cst env =
-  Cmap_env.find (Projection.constant cst) env.env_globals.env_projections
-
-let is_projection cst env =
-  Cmap_env.mem cst env.env_globals.env_projections
+let lookup_projection p env =
+  let mind,i = Projection.inductive p in
+  let mib = lookup_mind mind env in
+  (if not (Int.equal mib.mind_nparams (Projection.npars p))
+   then anomaly ~label:"lookup_projection" Pp.(str "Bad number of parameters on projection."));
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> anomaly ~label:"lookup_projection" Pp.(str "not a projection")
+  | PrimRecord infos ->
+    let _,_,typs = infos.(i) in
+    typs.(Projection.arg p)
+
+let get_projection env ind ~proj_arg =
+  let mib = lookup_mind (fst ind) env in
+  Declareops.inductive_make_projection ind mib ~proj_arg
+
+let get_projections env ind =
+  let mib = lookup_mind (fst ind) env in
+  Declareops.inductive_make_projections ind mib
 
 (* Mutual Inductives *)
 let polymorphic_ind (mind,i) env =
@@ -518,17 +529,9 @@ let template_polymorphic_pind (ind,u) env =
   
 let add_mind_key kn (mind, _ as mind_key) env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
-  let new_projections = match mind.mind_record with
-    | NotRecord | FakeRecord -> env.env_globals.env_projections
-    | PrimRecord projs ->
-      Array.fold_left (fun accu (id, kns, pbs) ->
-      Array.fold_left2 (fun accu kn pb ->
-          Cmap_env.add kn pb accu) accu kns pbs)
-        env.env_globals.env_projections projs
-  in
   let new_globals =
     { env.env_globals with
-        env_inductives = new_inds; env_projections = new_projections; } in
+        env_inductives = new_inds; } in
   { env with env_globals = new_globals }
 
 let add_mind kn mib env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0259dbbdda..f45b7be821 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -217,8 +217,11 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 (** {6 Primitive projections} *)
 
-val lookup_projection    : Names.Projection.t -> env -> projection_body
-val is_projection : Constant.t -> env -> bool
+(** Checks that the number of parameters is correct. *)
+val lookup_projection : Names.Projection.t -> env -> types
+
+val get_projection : env -> inductive -> proj_arg:int -> Names.Projection.Repr.t option
+val get_projections : env -> inductive -> Names.Projection.Repr.t array option
 
 (** {5 Inductive types } *)
 val lookup_mind_key : MutInd.t -> env -> mind_key
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5d45c2c1ad..d7eb865e0a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -796,7 +796,6 @@ let compute_projections (kn, i as ind) mib =
   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. *)
@@ -810,7 +809,7 @@ let compute_projections (kn, i as ind) mib =
       mkRel 1 :: List.map (lift 1) subst in
     subst
   in
-  let projections decl (i, j, kns, pbs, letsubst) =
+  let projections decl (i, j, labs, pbs, letsubst) =
     match decl with
     | LocalDef (na,c,t) ->
         (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
@@ -822,11 +821,12 @@ let compute_projections (kn, i as ind) mib =
         (* 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, letsubst)
+        (i, j+1, labs, pbs, letsubst)
     | 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:i 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
@@ -836,15 +836,13 @@ let compute_projections (kn, i as ind) mib =
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
-        let body = { proj_ind = ind; proj_npars = mib.mind_nparams;
-                      proj_arg = i; proj_type = projty; } in
-        (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
+        (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, kns, pbs, letsubst) =
+  let (_, _, labs, pbs, letsubst) =
     List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
   in
-    Array.of_list (List.rev kns),
+    Array.of_list (List.rev labs),
     Array.of_list (List.rev pbs)
 
 let abstract_inductive_universes iu =
@@ -954,8 +952,8 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
     (** The elimination criterion ensures that all projections can be defined. *)
     if Array.for_all is_record packets then
       let map i id =
-        let kn, projs = compute_projections (kn, i) mib in
-        (id, kn, projs)
+        let labs, projs = compute_projections (kn, i) mib in
+        (id, labs, projs)
       in
       try PrimRecord (Array.mapi map rid)
       with UndefinableExpansion -> FakeRecord
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7c36dac67d..cb09cfa827 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -42,6 +42,3 @@ 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 : inductive ->
-  mutual_inductive_body -> (Constant.t array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 88b00600e4..4d13a5fcb8 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -798,8 +798,7 @@ let rec subterm_specif renv stack t =
          (* We take the subterm specs of the constructor of the record *)
          let wf_args = (dest_subterms wf).(0) in
          (* We extract the tree of the projected argument *)
-         let pb = lookup_projection p renv.env in
-         let n = pb.proj_arg in
+         let n = Projection.arg p in
          spec_of_tree (List.nth wf_args n)
        | Dead_code -> Dead_code
        | Not_subterm -> Not_subterm)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index a47af56ca5..b35b9dda31 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -332,6 +332,12 @@ let subst_constant sub con =
   try fst (subst_con0 sub (con,Univ.Instance.empty))
   with No_subst -> con
 
+let subst_proj_repr sub p =
+  Projection.Repr.map (subst_mind sub) p
+
+let subst_proj sub p =
+  Projection.map (subst_mind sub) p
+
 (* Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
    Does the user mean "Unfold X.t" or does she mean "Unfold y"
@@ -346,11 +352,7 @@ let rec map_kn f f' c =
     match kind c with
       | Const kn -> (try snd (f' kn) with No_subst -> c)
       | Proj (p,t) -> 
-          let p' = 
-	    try
-	      Projection.map (fun kn -> fst (f' (kn,Univ.Instance.empty))) p
-	    with No_subst -> p
-	  in
+          let p' = Projection.map f p in
 	  let t' = func t in
 	    if p' == p && t' == t then c
 	    else mkProj (p', t')
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 76a1d173b9..2e5211c770 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -147,6 +147,9 @@ val subst_con_kn :
 val subst_constant :
   substitution -> Constant.t -> Constant.t
 
+val subst_proj_repr : substitution -> Projection.Repr.t -> Projection.Repr.t
+val subst_proj : substitution -> Projection.t -> Projection.t
+
 (** Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
    Does the user mean "Unfold X.t" or does she mean "Unfold y"
diff --git a/kernel/names.ml b/kernel/names.ml
index 1d2a7c4ce5..e1d70e8111 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -771,29 +771,141 @@ type module_path = ModPath.t =
 
 module Projection =
 struct
-  type t = Constant.t * bool
+  module Repr = struct
+    type t =
+      { proj_ind : inductive;
+        proj_npars : int;
+        proj_arg : int;
+        proj_name : Label.t; }
+
+    let make proj_ind ~proj_npars ~proj_arg proj_name =
+      {proj_ind;proj_npars;proj_arg;proj_name}
+
+    let inductive c = c.proj_ind
+
+    let mind c = fst c.proj_ind
+
+    let constant c = KerPair.change_label (mind c) c.proj_name
+
+    let label c = c.proj_name
+
+    let npars c = c.proj_npars
+
+    let arg c = c.proj_arg
+
+    let equal a b =
+      eq_ind a.proj_ind b.proj_ind && Int.equal a.proj_arg b.proj_arg
+
+    let hash p =
+      Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind)
+
+    module SyntacticOrd = struct
+      let compare a b =
+        let c = ind_syntactic_ord a.proj_ind b.proj_ind in
+        if c == 0 then Int.compare a.proj_arg b.proj_arg
+        else c
+
+      let equal a b =
+        a.proj_arg == b.proj_arg && eq_syntactic_ind a.proj_ind b.proj_ind
+
+      let hash p =
+        Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind)
+    end
+    module CanOrd = struct
+      let compare a b =
+        let c = ind_ord a.proj_ind b.proj_ind in
+        if c == 0 then Int.compare a.proj_arg b.proj_arg
+        else c
+
+      let equal a b =
+        a.proj_arg == b.proj_arg && eq_ind a.proj_ind b.proj_ind
+
+      let hash p =
+        Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind)
+    end
+    module UserOrd = struct
+      let compare a b =
+        let c = ind_user_ord a.proj_ind b.proj_ind in
+        if c == 0 then Int.compare a.proj_arg b.proj_arg
+        else c
+
+      let equal a b =
+        a.proj_arg == b.proj_arg && eq_user_ind a.proj_ind b.proj_ind
+
+      let hash p =
+        Hashset.Combine.combinesmall p.proj_arg (ind_user_hash p.proj_ind)
+    end
+
+    let compare a b =
+      let c = ind_ord a.proj_ind b.proj_ind in
+      if c == 0 then Int.compare a.proj_arg b.proj_arg
+      else c
+
+    module Self_Hashcons = struct
+      type nonrec t = t
+      type u = (inductive -> inductive) * (Id.t -> Id.t)
+      let hashcons (hind,hid) p =
+        { proj_ind = hind p.proj_ind;
+          proj_npars = p.proj_npars;
+          proj_arg = p.proj_arg;
+          proj_name = hid p.proj_name }
+      let eq p p' =
+        p == p' || (p.proj_ind == p'.proj_ind && p.proj_npars == p'.proj_npars && p.proj_arg == p'.proj_arg && p.proj_name == p'.proj_name)
+      let hash = hash
+    end
+    module HashRepr = Hashcons.Make(Self_Hashcons)
+    let hcons = Hashcons.simple_hcons HashRepr.generate HashRepr.hcons (hcons_ind,Id.hcons)
+
+    let map_npars f p =
+      let ind = fst p.proj_ind in
+      let npars = p.proj_npars in
+      let ind', npars' = f ind npars in
+      if ind == ind' && npars == npars' then p
+      else {p with proj_ind = (ind',snd p.proj_ind); proj_npars = npars'}
+
+    let map f p = map_npars (fun mind n -> f mind, n) p
+
+    let to_string p = Constant.to_string (constant p)
+    let print p = Constant.print (constant p)
+  end
+
+  type t = Repr.t * bool
 
   let make c b = (c, b)
 
-  let constant = fst
+  let mind (c,_) = Repr.mind c
+  let inductive (c,_) = Repr.inductive c
+  let npars (c,_) = Repr.npars c
+  let arg (c,_) = Repr.arg c
+  let constant (c,_) = Repr.constant c
+  let label (c,_) = Repr.label c
+  let repr = fst
   let unfolded = snd
   let unfold (c, b as p) = if b then p else (c, true)
-  let equal (c, b) (c', b') = Constant.equal c c' && b == b'
 
-  let hash (c, b) = (if b then 0 else 1) + Constant.hash c
+  let equal (c, b) (c', b') = Repr.equal c c' && b == b'
+
+  let hash (c, b) = (if b then 0 else 1) + Repr.hash c
 
   module SyntacticOrd = struct
     let compare (c, b) (c', b') =
-      if b = b' then Constant.SyntacticOrd.compare c c' else -1
+      if b = b' then Repr.SyntacticOrd.compare c c' else -1
+    let equal (c, b as x) (c', b' as x') =
+      x == x' || b = b' && Repr.SyntacticOrd.equal c c'
+    let hash (c, b) = (if b then 0 else 1) + Repr.SyntacticOrd.hash c
+  end
+  module CanOrd = struct
+    let compare (c, b) (c', b') =
+      if b = b' then Repr.CanOrd.compare c c' else -1
     let equal (c, b as x) (c', b' as x') =
-      x == x' || b = b' && Constant.SyntacticOrd.equal c c'
-    let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c
+      x == x' || b = b' && Repr.CanOrd.equal c c'
+    let hash (c, b) = (if b then 0 else 1) + Repr.CanOrd.hash c
   end
 
   module Self_Hashcons =
     struct
       type nonrec t = t
-      type u = Constant.t -> Constant.t
+      type u = Repr.t -> Repr.t
       let hashcons hc (c,b) = (hc c,b)
       let eq ((c,b) as x) ((c',b') as y) =
         x == y || (c == c' && b == b')
@@ -802,15 +914,19 @@ struct
 
   module HashProjection = Hashcons.Make(Self_Hashcons)
 
-  let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons hcons_con
+  let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons Repr.hcons
 
   let compare (c, b) (c', b') =
-    if b == b' then Constant.CanOrd.compare c c'
+    if b == b' then Repr.compare c c'
     else if b then 1 else -1
 
   let map f (c, b as x) =
-    let c' = f c in
-      if c' == c then x else (c', b)
+    let c' = Repr.map f c in
+    if c' == c then x else (c', b)
+
+  let map_npars f (c, b as x) =
+    let c' = Repr.map_npars f c in
+    if c' == c then x else (c', b)
 
   let to_string p = Constant.to_string (constant p)
   let print p = Constant.print (constant p)
diff --git a/kernel/names.mli b/kernel/names.mli
index 4eb5adb62f..1cdf5c2402 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -549,17 +549,68 @@ type module_path = ModPath.t =
 [@@ocaml.deprecated "Alias type"]
 
 module Projection : sig
-  type t
+  module Repr : sig
+    type t
+
+    val make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t
+
+    module SyntacticOrd : sig
+      val compare : t -> t -> int
+      val equal : t -> t -> bool
+      val hash : t -> int
+    end
+    module CanOrd : sig
+      val compare : t -> t -> int
+      val equal : t -> t -> bool
+      val hash : t -> int
+    end
+    module UserOrd : sig
+      val compare : t -> t -> int
+      val equal : t -> t -> bool
+      val hash : t -> int
+    end
+
+    val constant : t -> Constant.t
+    (** Don't use this if you don't have to. *)
+
+    val inductive : t -> inductive
+    val mind : t -> MutInd.t
+    val npars : t -> int
+    val arg : t -> int
+    val label : t -> Label.t
+
+    val equal : t -> t -> bool
+    val hash : t -> int
+    val compare : t -> t -> int
+
+    val map : (MutInd.t -> MutInd.t) -> t -> t
+    val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
+
+    val print : t -> Pp.t
+    val to_string : t -> string
+  end
+  type t (* = Repr.t * bool *)
 
-  val make : Constant.t -> bool -> t
+  val make : Repr.t -> bool -> t
+  val repr : t -> Repr.t
 
   module SyntacticOrd : sig
     val compare : t -> t -> int
     val equal : t -> t -> bool
     val hash : t -> int
   end
+  module CanOrd : sig
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
 
   val constant : t -> Constant.t
+  val mind : t -> MutInd.t
+  val inductive : t -> inductive
+  val npars : t -> int
+  val arg : t -> int
+  val label : t -> Label.t
   val unfolded : t -> bool
   val unfold : t -> t
 
@@ -570,7 +621,8 @@ module Projection : sig
 
   val compare : t -> t -> int
 
-  val map : (Constant.t -> Constant.t) -> t -> t
+  val map : (MutInd.t -> MutInd.t) -> t -> t
+  val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
 
   val to_string : t -> string
   val print : t -> Pp.t
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ec6c5b297a..cc35a70cbf 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1980,8 +1980,7 @@ let compile_mind mb mind stack =
 	       (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
     in
     let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
-    let add_proj j acc pb =
-      let () = assert (eq_ind ind pb.proj_ind) in
+    let add_proj proj_arg acc pb =
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
       let ci = { ci_ind = ind; ci_npar = nparams;
@@ -1995,14 +1994,14 @@ let compile_mind mb mind stack =
       let _, arity = tbl.(0) in
       let ci_uid = fresh_lname Anonymous in
       let cargs = Array.init arity
-        (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None)
+        (fun i -> if Int.equal i proj_arg then Some ci_uid else None)
       in
       let i = push_symbol (SymbProj (ind, j)) in
       let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
       let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
       let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
-      let gn = Gproj ("", ind, pb.proj_arg) in
+      let gn = Gproj ("", ind, proj_arg) in
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
     in
     let projs = match mb.mind_record with
@@ -2070,8 +2069,7 @@ let compile_deps env sigma prefix ~interactive init t =
       comp_stack, (mind_updates, const_updates)
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
-    let pb = lookup_projection p env in
-    let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in
+    let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in
     aux env lvl init c
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index a5cdd0a19c..cec0ee57d5 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -464,10 +464,9 @@ let rec lambda_of_constr cache env sigma c =
   | Construct _ ->  lambda_of_app cache env sigma c empty_args
 
   | Proj (p, c) ->
-    let pb = lookup_projection p env in
-    let ind = pb.proj_ind in
+    let ind = Projection.inductive p in
     let prefix = get_mind_prefix env (fst ind) in
-    mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr cache env sigma c|]
+    mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
 
   | Case(ci,t,a,branches) ->  
       let (mind,i as ind) = ci.ci_ind in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 3228a155f3..c701b53fe4 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -53,7 +53,7 @@ let compare_stack_shape stk1 stk2 =
     | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
     | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
-    | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
+    | (Zproj p1::s1, Zproj p2::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
     | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
@@ -66,7 +66,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Constant.t * lift
+  | Zlproj of Projection.Repr.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -96,8 +96,8 @@ let pure_stack lfts stk =
             | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
             | (Zapp a, (l,pstk)) ->
                 (l,zlapp (map_lift l a) pstk)
-	    | (Zproj (n,m,c), (l,pstk)) ->
-		(l, Zlproj (c,l)::pstk)
+            | (Zproj p, (l,pstk)) ->
+                (l, Zlproj (p,l)::pstk)
             | (Zfix(fx,a),(l,pstk)) ->
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
@@ -297,7 +297,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
             | (Zlapp a1,Zlapp a2) -> 
 	       Array.fold_right2 f a1 a2 cu1
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-	      if not (Constant.equal c1 c2) then 
+              if not (Projection.Repr.equal c1 c2) then
 		raise NotConvertible
 	      else cu1
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
@@ -408,7 +408,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         | Some s2 ->
           eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
 	| None -> 
-          if Constant.equal (Projection.constant p1) (Projection.constant p2)
+          if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
 	     && compare_stack_shape v1 v2 then
             let el1 = el_stack lft1 v1 in
             let el2 = el_stack lft2 v2 in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7c0057696e..7f36f3813f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -296,13 +296,13 @@ let type_of_case env ci p pt c ct lf lft =
   rslty
 
 let type_of_projection env p c ct =
-  let pb = lookup_projection p env in
+  let pty = lookup_projection p env in
   let (ind,u), args =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct)
   in
-  assert(eq_ind pb.proj_ind ind);
-  let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
+  assert(eq_ind (Projection.inductive p) ind);
+  let ty = Vars.subst_instance_constr u pty in
   substl (c :: CList.rev args) ty
       
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 4e4168922d..d19bea5199 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -139,7 +139,7 @@ and conv_stack env k stk1 stk2 cu =
 	conv_stack env k stk1 stk2 !rcu
       else raise NotConvertible
   | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
-    if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
+    if Projection.Repr.equal p1 p2 then conv_stack env k stk1 stk2 cu
     else raise NotConvertible
   | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
   | Zproj _ :: _, _ -> raise NotConvertible
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 8524c44d21..d6d9312938 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -150,7 +150,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix*arguments  (* Possibly empty *)
   | Zswitch of vswitch
-  | Zproj of Constant.t (* name of the projection *)
+  | Zproj of Projection.Repr.t (* name of the projection *)
 
 type stack = zipper list
 
@@ -354,7 +354,7 @@ let val_of_constant c = val_of_idkey (ConstKey c)
 let val_of_evar evk = val_of_idkey (EvarKey evk)
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
-external val_of_proj_name : Constant.t -> values = "%identity"
+external val_of_proj_name : Projection.Repr.t -> values = "%identity"
 
 (*************************************************)
 (** Operations manipulating data types ***********)
@@ -553,4 +553,4 @@ and pr_zipper z =
   | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")"
   | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
   | Zswitch s -> str "Zswitch(...)"
-  | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")")
+  | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")")
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 08d05a038c..6eedcf1d37 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -81,7 +81,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix * arguments  (** might be empty *)
   | Zswitch of vswitch
-  | Zproj of Constant.t (* name of the projection *)
+  | Zproj of Projection.Repr.t (* name of the projection *)
 
 type stack = zipper list
 
@@ -108,11 +108,11 @@ val val_of_rel : int -> values
 val val_of_named : Id.t -> values
 val val_of_constant : Constant.t -> values
 val val_of_evar : Evar.t -> values
-val val_of_proj : Constant.t -> values -> values
+val val_of_proj : Projection.Repr.t -> values -> values
 val val_of_atom : atom -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
-external val_of_proj_name : Constant.t -> values = "%identity"
+external val_of_proj_name : Projection.Repr.t -> values = "%identity"
 
 (** Destructors *)
 
diff --git a/library/lib.ml b/library/lib.ml
index a20de55bf6..8b83261e48 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -656,6 +656,14 @@ let discharge_kn kn =
 let discharge_con cst =
   if con_defined_in_sec cst then Globnames.pop_con cst else cst
 
+let discharge_proj_repr =
+  Projection.Repr.map_npars (fun mind npars ->
+      if not (defined_in_sec mind) then mind, npars
+      else
+        let modlist = replacement_context () in
+        let _, newpars = Mindmap.find mind (snd modlist) in
+        Globnames.pop_kn mind, npars + Array.length newpars)
+
 let discharge_inductive (kn,i) =
   (discharge_kn kn,i)
 
diff --git a/library/lib.mli b/library/lib.mli
index 5abfccfc7d..c6856a55b4 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -189,6 +189,7 @@ val replacement_context : unit -> Opaqueproof.work_list
 
 val discharge_kn :  MutInd.t -> MutInd.t
 val discharge_con : Constant.t -> Constant.t
+val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t
 val discharge_global : GlobRef.t -> GlobRef.t
 val discharge_inductive : inductive -> inductive
 val discharge_abstract_universe_context :
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 4a691e442c..ce620d5312 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -460,7 +460,7 @@ let rec canonize_name sigma c =
           mkApp (func ct,Array.Smart.map func l)
       | Proj(p,c) ->
 	let p' = Projection.map (fun kn ->
-          Constant.make1 (Constant.canonical kn)) p in 
+          MutInd.make1 (MutInd.canonical kn)) p in
 	  (mkProj (p', func c))
       | _ -> c
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 04ff11fc49..2eaa6146e1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -84,8 +84,8 @@ let rec decompose_term env sigma t=
 	let canon_const = Constant.make1 (Constant.canonical c) in 
 	  (Symb (Constr.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
-	let canon_const kn = Constant.make1 (Constant.canonical kn) in 
-	let p' = Projection.map canon_const p in
+        let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in
+        let p' = Projection.map canon_mind p in
 	let c = Retyping.expand_projection env sigma p' c [] in
 	decompose_term env sigma c
     | _ ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 71e09992cc..67c605ea1d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1065,13 +1065,13 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
 	  | Def c ->
-             (match Environ.is_projection kn env with
-              | false -> mk_typ (get_body c)
-              | true ->
-                let pb = lookup_projection (Projection.make kn false) env in
-                let ind = pb.Declarations.proj_ind in
+             (match Recordops.find_primitive_projection kn with
+              | None -> mk_typ (get_body c)
+              | Some p ->
+                let p = Projection.make p false in
+                let ind = Projection.inductive p in
                 let bodies = Inductiveops.legacy_match_projection env ind in
-                let body = bodies.(pb.Declarations.proj_arg) in
+                let body = bodies.(Projection.arg p) in
                 mk_typ (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
@@ -1081,13 +1081,13 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
 	  | Def c ->
-             (match Environ.is_projection kn env with
-              | false -> mk_def (get_body c)
-              | true ->
-                let pb = lookup_projection (Projection.make kn false) env in
-                let ind = pb.Declarations.proj_ind in
+             (match Recordops.find_primitive_projection kn with
+              | None -> mk_def (get_body c)
+              | Some p ->
+                let p = Projection.make p false in
+                let ind = Projection.inductive p in
                 let bodies = Inductiveops.legacy_match_projection env ind in
-                let body = bodies.(pb.Declarations.proj_arg) in
+                let body = bodies.(Projection.arg p) in
                 mk_def (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
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
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 748e0362c4..09b2e59cea 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -299,16 +299,16 @@ let strip_params env sigma c =
   match EConstr.kind sigma c with
   | App (f, args) -> 
     (match EConstr.kind sigma f with
-    | Const (p,_) ->
-      let p = Projection.make p false in
-      (match lookup_projection p env with
-       | pb ->
-         let n = pb.Declarations.proj_npars in
-         if Array.length args > n then
-           mkApp (mkProj (p, args.(n)),
-                  Array.sub args (n+1) (Array.length args - (n + 1)))
+    | Const (cst,_) ->
+      (match Recordops.find_primitive_projection cst with
+       | Some p ->
+         let p = Projection.make p false in
+         let npars = Projection.npars p in
+         if Array.length args > npars then
+           mkApp (mkProj (p, args.(npars)),
+                  Array.sub args (npars+1) (Array.length args - (npars + 1)))
          else c
-       | exception Not_found -> c)
+       | None -> c)
     | _ -> c)
   | _ -> c
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 928530744a..5fc34619e8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1581,9 +1581,10 @@ let make_projection env sigma params cstr sign elim i n c u =
       | Some proj ->
 	  let args = Context.Rel.to_extended_vect mkRel 0 sign in
 	  let proj =
-	    if Environ.is_projection proj env then
+            match Recordops.find_primitive_projection proj with
+            | Some proj ->
 	      mkProj (Projection.make proj false, mkApp (c, args))
-	    else
+            | None ->
 	      mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
 		[|mkApp (c, args)|])
 	  in
diff --git a/vernac/class.ml b/vernac/class.ml
index e425e6474d..614b2181d9 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -73,7 +73,7 @@ let check_reference_arity ref =
 let check_arity = function
   | CL_FUN | CL_SORT -> ()
   | CL_CONST cst -> check_reference_arity (ConstRef cst)
-  | CL_PROJ cst -> check_reference_arity (ConstRef cst)
+  | CL_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p))
   | CL_SECVAR id -> check_reference_arity (VarRef id)
   | CL_IND kn -> check_reference_arity (IndRef kn)
 
@@ -92,8 +92,8 @@ let uniform_cond sigma ctx lt =
 
 let class_of_global = function
   | ConstRef sp -> 
-    if Environ.is_projection sp (Global.env ()) 
-    then CL_PROJ sp else CL_CONST sp
+    (match Recordops.find_primitive_projection sp with
+     | Some p -> CL_PROJ p | None -> CL_CONST sp)
   | IndRef sp -> CL_IND sp
   | VarRef id -> CL_SECVAR id
   | ConstructRef _ as c ->
@@ -143,8 +143,8 @@ let get_target t ind =
     CL_FUN
   else
     match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
-    | CL_CONST p when Environ.is_projection p (Global.env ()) -> 
-      CL_PROJ p
+    | CL_CONST p when Recordops.is_primitive_projection p ->
+      CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
     | x -> x
       
 let strength_of_cl = function
@@ -165,7 +165,8 @@ let get_strength stre ref cls clt =
 let ident_key_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+  | CL_CONST sp -> Label.to_string (Constant.label sp)
+  | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp)
   | CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
   | CL_SECVAR id -> Id.to_string id
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a8ce7d25a..6b5c538df2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -324,12 +324,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
 	  | Name fid -> try
 	    let kn, term = 
 	      if is_local_assum decl && primitive then
-		(** Already defined in the kernel silently *)
-                let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
-                let kn = destConstRef gr in
+                let p = Projection.Repr.make indsp
+                    ~proj_npars:mib.mind_nparams
+                    ~proj_arg:i
+                    (Label.of_id fid)
+                in
+                (** Already defined by declare_mind silently *)
+                let kn = Projection.Repr.constant p in
                 Declare.definition_message fid;
-                UnivNames.register_universe_binders gr ubinders;
-                kn, mkProj (Projection.make kn false,mkRel 1)
+                UnivNames.register_universe_binders (ConstRef kn) ubinders;
+                kn, mkProj (Projection.make p false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
 		let body = match decl with