Merge PR #7908: Projections use index representation

30 files changed, 330 insertions, 162 deletions

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..9a1224aab2 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -128,8 +128,7 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
-  | Kproj of int * Constant.t  (* index of the projected argument,
-                                           name of projection *)
+  | Kproj of Projection.Repr.t
   | Kensurestackcapacity of int
 (* spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (* jump to label *)
@@ -311,7 +310,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 p -> str "proj " ++ Projection.Repr.print p
 
   | Kensurestackcapacity size -> str "growstack " ++ int size
 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index de21401b31..f17a1e657e 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -88,8 +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,
-                                            name of projection *)
+  | Kproj of Projection.Repr.t
   | Kensurestackcapacity of int
 
 (** spiwack: instructions concerning integers *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 6677db2fd9..4613cd3214 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -492,8 +492,8 @@ let rec compile_lam env cenv lam sz cont =
 
   | Lval v -> compile_structured_constant cenv v sz cont
 
-  | Lproj (n,kn,arg) ->
-     compile_lam env cenv arg sz (Kproj (n,kn) :: cont)
+  | Lproj (p,arg) ->
+     compile_lam env cenv arg sz (Kproj p :: cont)
 
   | Lvar id -> pos_named id cenv :: cont
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2426255e48..ca24f9b689 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
@@ -284,7 +284,7 @@ let emit_instr env = function
       if n <= 1 then out env (opSETFIELD0+n)
       else (out env opSETFIELD;out_int env n)
   | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
-  | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_proj_name env p
+  | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
   | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
   (* spiwack *)
   | Kbranch lbl -> out env opBRANCH; out_label env lbl
@@ -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..171ca38830 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 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..7c00e40fb0 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -111,9 +111,9 @@ let rec pp_lam lam =
       (str "(PRIM " ++ pr_con kn ++  spc() ++
        prlist_with_sep spc pp_lam  (Array.to_list args) ++
        str")")
-  | Lproj(i,kn,arg) ->
+  | Lproj(p,arg) ->
     hov 1
-      (str "(proj#" ++ int i ++ spc() ++ pr_con kn ++ str "(" ++ pp_lam arg
+      (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg
        ++ str ")")
   | Luint _ ->
     str "(uint)"
@@ -205,9 +205,9 @@ let rec map_lam_with_binders g f n lam =
   | Lprim(kn,ar,op,args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Lprim(kn,ar,op,args')
-  | Lproj(i,kn,arg) ->
+  | Lproj(p,arg) ->
     let arg' = f n arg in
-    if arg == arg' then lam else Lproj(i,kn,arg')
+    if arg == arg' then lam else Lproj(p,arg')
   | Luint u ->
     let u' = map_uint g f n u in
     if u == u' then lam else Luint u'
@@ -376,7 +376,7 @@ let rec occurrence k kind lam =
     let kind = occurrence_args k kind ltypes in
     let _ = occurrence_args (k+Array.length ids) false lbodies in
     kind
-  | Lproj(_,_,arg) ->
+  | Lproj(_,arg) ->
     occurrence k kind arg
   | Luint u -> occurrence_uint k kind u
 
@@ -708,10 +708,8 @@ 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 lc = lambda_of_constr env c in
-    Lproj (n,Projection.constant p,lc)
+    Lproj (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 *)