28 files changed, 274 insertions, 188 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1edce17bd..93ca9dc5e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1425,8 +1425,9 @@ and match_current pb (initial,tomatch) =
 	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
           let pred = nf_betaiota pb.env !(pb.evdref) pred in
 	  let case =
-	    make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
+            make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
 	  in
+          let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in
 	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
 	  { uj_val = applist (case, inst);
 	    uj_type = prod_applist !(pb.evdref) typ inst }
@@ -2103,7 +2104,7 @@ let mk_JMeq_refl evdref typ x =
 
 let hole na = DAst.make @@
   GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
-         Misctypes.IntroAnonymous, None)
+         IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e6cfe1f76..23a985dc3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -27,7 +27,6 @@ open Libnames
 open Globnames
 open Nametab
 open Mod_subst
-open Misctypes
 open Decl_kinds
 open Context.Named.Declaration
 open Ltac_pretype
@@ -88,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) =
 
 module PrintingInductiveMake =
   functor (Test : sig
-     val encode : reference -> inductive
+     val encode : qualid -> inductive
      val member_message : Pp.t -> bool -> Pp.t
      val field : string
      val title : string
@@ -691,7 +690,9 @@ and detype_r d flags avoid env sigma t =
 	  let c' = 
 	    try 
 	      let pb = Environ.lookup_projection p (snd env) in
-	      let body = pb.Declarations.proj_body in
+              let ind = pb.Declarations.proj_ind in
+              let bodies = Inductiveops.legacy_match_projection (snd env) ind in
+              let body = bodies.(pb.Declarations.proj_arg) in
 	      let ty = Retyping.get_type_of (snd env) sigma c in
 	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
 	      let body' = strip_lam_assum body in
@@ -1027,7 +1028,7 @@ let rec subst_glob_constr subst = DAst.map (function
 
   | GCast (r1,k) as raw ->
       let r1' = subst_glob_constr subst r1 in
-      let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
+      let k' = smartmap_cast_type (subst_glob_constr subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
 
   | GProj (p,c) as raw ->
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5310455fe..8695d52b1 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -87,7 +87,7 @@ val subst_genarg_hook :
 
 module PrintingInductiveMake :
   functor (Test : sig
-    val encode : Libnames.reference -> Names.inductive
+    val encode : Libnames.qualid -> Names.inductive
     val member_message : Pp.t -> bool -> Pp.t
     val field : string
     val title : string
@@ -95,7 +95,7 @@ module PrintingInductiveMake :
     sig
       type t = Names.inductive
       val compare : t -> t -> int
-      val encode : Libnames.reference -> Names.inductive
+      val encode : Libnames.qualid -> Names.inductive
       val subst : substitution -> t -> t
       val printer : t -> Pp.t
       val key : Goptions.option_name
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6d08f66c1..a71ef6508 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -510,7 +510,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
         let tM = Stack.zip evd apprM in
 	  miller_pfenning on_left
 	    (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
-	      switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
+              switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
 	    else quick_fail i)
 	  ev lF tM i
     and consume (termF,skF as apprF) (termM,skM as apprM) i = 
@@ -578,7 +578,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                          i,mkEvar ev
                        else
                          i,Stack.zip evd apprF in
-		     switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
+                     switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i))
 	               tF tR
 		   else
                      UnifFailure (evd,OccurCheck (fst ev,tR)))])
@@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 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
-    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
+    | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite ->
+      let (_, projs, _) = info.(snd ind) in
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aefae1ecc..8afb9b942 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -929,7 +929,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
     with Not_found ->
       match expand_alias_once evd aliases t with
       | None -> raise Not_found
-      | Some c -> aux k c in
+      | Some c -> aux k (lift k c) in
   try
     let c = aux 0 c_in_env_extended_with_k_binders in
     Invertible (UniqueProjection (c,!effects))
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
index fa522e9c3..606a6ebea 100644
--- a/pretyping/geninterp.mli
+++ b/pretyping/geninterp.mli
@@ -42,8 +42,8 @@ sig
 
 end
 
-module ValTMap (M : Dyn.TParam) :
-  Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+module ValTMap (Value : Dyn.ValueS) :
+  Dyn.MapS with type 'a key = 'a Val.typ and type 'a value = 'a Value.t
 
 (** Dynamic types for toplevel values. While the generic types permit to relate
     objects at various levels of interpretation, toplevel values are wearing
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 63618c918..ba193da60 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -11,10 +11,8 @@
 open Util
 open CAst
 open Names
-open Constr
 open Nameops
 open Globnames
-open Misctypes
 open Glob_term
 open Evar_kinds
 open Ltac_pretype
@@ -48,12 +46,20 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
+
+let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
+| GProp, GProp -> true
+| GSet, GSet -> true
+| GType l1, GType l2 ->
+   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2
+| _ -> false
+
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Decl_kinds.Explicit, Decl_kinds.Explicit -> true
   | Decl_kinds.Implicit, Decl_kinds.Implicit -> true
   | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false
 
-let case_style_eq s1 s2 = match s1, s2 with
+let case_style_eq s1 s2 = let open Constr in match s1, s2 with
   | LetStyle, LetStyle -> true
   | IfStyle, IfStyle -> true
   | LetPatternStyle, LetPatternStyle -> true
@@ -141,10 +147,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
     Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
     Array.equal f c1 c2 && Array.equal f t1 t2
-  | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+  | GSort s1, GSort s2 -> glob_sort_eq s1 s2
   | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
     Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
-    Miscops.intro_pattern_naming_eq nam1 nam2
+    Namegen.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
   | GProj (p1, t1), GProj (p2, t2) ->
@@ -154,6 +160,21 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
+(** Mapping [cast_type] *)
+
+let map_cast_type f = function
+  | CastConv a -> CastConv (f a)
+  | CastVM a -> CastVM (f a)
+  | CastCoerce -> CastCoerce
+  | CastNative a -> CastNative (f a)
+
+let smartmap_cast_type f c =
+  match c with
+    | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
+    | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
+    | CastCoerce -> CastCoerce
+    | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
+
 let map_glob_constr_left_to_right f = DAst.map (function
   | GApp (g,args) ->
       let comp1 = f g in
@@ -194,7 +215,7 @@ let map_glob_constr_left_to_right f = DAst.map (function
       GRec (fk,idl,comp1,comp2,comp3)
   | GCast (c,k) ->
       let comp1 = f c in
-      let comp2 = Miscops.map_cast_type f k in
+      let comp2 = map_cast_type f k in
       GCast (comp1,comp2)
   | GProj (p,c) ->
     GProj (p, f c)
@@ -248,8 +269,9 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
   | GCases (_,rtntypopt,tml,pl) ->
     let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in
     let fold_tomatch (v',acc) (tm,(na,onal)) =
-      (Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
-                        (Name.fold_right g na v') onal,
+      ((if rtntypopt = None then v' else
+       Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'')
+                        (Name.fold_right g na v') onal),
        f v acc tm) in
     let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
     let acc = Option.fold_left (f v') acc rtntypopt in
@@ -260,6 +282,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
   | GIf (c,rtntyp,b1,b2) ->
     f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
   | GRec (_,idl,bll,tyl,bv) ->
+    let v' = Array.fold_right g idl v in
     let f' i acc fid =
       let v,acc =
 	List.fold_left
@@ -267,7 +290,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
             (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty))
           (v,acc)
           bll.(i) in
-      f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
+      f v' (f v acc tyl.(i)) (bv.(i)) in
     Array.fold_left_i f' acc idl
   | GCast (c,k) ->
     let acc = match k with
@@ -391,8 +414,10 @@ let loc_of_glob_constr c = c.CAst.loc
 (**********************************************************************)
 (* Alpha-renaming                                                     *)
 
+exception UnsoundRenaming
+
 let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
-let test_id l id = if collide_id l id then raise Not_found
+let test_id l id = if collide_id l id then raise UnsoundRenaming
 let test_na l na = Name.iter (test_id l) na
 
 let update_subst na l =
@@ -406,8 +431,6 @@ let update_subst na l =
      else na,l)
     na (na,l)
 
-exception UnsoundRenaming
-
 let rename_var l id =
   try
     let id' = Id.List.assoc id l in
@@ -539,7 +562,7 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo
   | PatVar (Name id) when not isclosed ->
       GVar id
   | PatVar Anonymous when not isclosed ->
-      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None)
+      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None)
   | _ -> raise Not_found
   ) x
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 124440f5d..c967f4e88 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,8 @@ open Glob_term
 
 (** Equalities *)
 
+val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
+
 val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 val alias_of_pat : 'a cases_pattern_g -> Name.t
@@ -20,10 +22,15 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t
 val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
 
 val cast_type_eq : ('a -> 'a -> bool) ->
-  'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+  'a cast_type -> 'a cast_type -> bool
 
 val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool
 
+(** Mapping [cast_type] *)
+
+val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
+val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
+
 (** Operations on [glob_constr] *)
 
 val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 6ecb479e6..86245d479 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -18,7 +18,6 @@
 
 open Names
 open Decl_kinds
-open Misctypes
 
 type existential_name = Id.t
 
@@ -34,13 +33,21 @@ type 'a universe_kind =
   | UUnknown
   | UNamed of 'a
 
-type level_info = Libnames.reference universe_kind
+type level_info = Libnames.qualid universe_kind
 type glob_level = level_info glob_sort_gen
 type glob_constraint = glob_level * Univ.constraint_type * glob_level
 
-type sort_info = (Libnames.reference * int) option list
+type sort_info = (Libnames.qualid * int) option list
 type glob_sort = sort_info glob_sort_gen
 
+(** Casts *)
+
+type 'a cast_type =
+  | CastConv of 'a
+  | CastVM of 'a
+  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
+  | CastNative of 'a
+
 (**  The kind of patterns that occurs in "match ... with ... end"
 
      locs here refers to the ident's location, not whole pat *)
@@ -73,7 +80,7 @@ type 'a glob_constr_r =
   | GRec  of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
              'a glob_constr_g array * 'a glob_constr_g array
   | GSort of glob_sort
-  | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option
+  | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
   | GProj of Projection.t * 'a glob_constr_g
 and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 27b029aad..4ab932723 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -304,7 +304,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   process_constr env 0 f (List.rev cstr.cs_args, recargs)
 
 (* Main function *)
-let mis_make_indrec env sigma listdepkind mib u =
+let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let evdref = ref sigma in
@@ -469,7 +469,7 @@ let mis_make_indrec env sigma listdepkind mib u =
     (* Body on make_one_rec *)
     let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in
 
-      if (mis_is_recursive_subset
+      if force_mutual || (mis_is_recursive_subset
 	(List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind)
 	mipi.mind_recargs)
       then
@@ -558,7 +558,7 @@ let check_arities env listdepkind =
 	    [] listdepkind
   in true
 
-let build_mutual_induction_scheme env sigma = function
+let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
   | ((mind,u),dep,s)::lrecspec ->
       let (mib,mip) = lookup_mind_specif env mind in
       if dep && not (Inductiveops.has_dependent_elim mib) then
@@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function
 	   lrecspec)
       in
       let _ = check_arities env listdepkind in
-      mis_make_indrec env sigma listdepkind mib u
+      mis_make_indrec env sigma ~force_mutual listdepkind mib u
   | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.")
 
 let build_induction_scheme env sigma pind dep kind =
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index d87a19d28..de9d3a0ab 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -47,7 +47,8 @@ val build_induction_scheme : env -> evar_map -> pinductive ->
 (** Builds mutual (recursive) induction schemes *)
 
 val build_mutual_induction_scheme :
-  env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list
+  env -> evar_map -> ?force_mutual:bool ->
+  (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list
 
 (** Scheme combinators *)
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b1ab2d2b7..d599afe69 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 
 let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite == BiFinite
-  | _ -> true
+  | PrimRecord _ -> mib.mind_finite == BiFinite
+  | NotRecord | FakeRecord -> true
 
 (* Annotation for cases *)
 let make_case_info env ind style =
@@ -346,8 +346,10 @@ let get_constructors env (ind,params) =
 let get_projections env (ind,params) =
   let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
     match mib.mind_record with
-    | Some (Some (id, projs, pbs)) -> Some projs
-    | _ -> None
+    | PrimRecord infos ->
+      let (_, projs, _) = infos.(snd (fst ind)) in
+      Some projs
+    | NotRecord | FakeRecord -> None
 
 let make_case_or_project env sigma indf ci pred c branches =
   let open EConstr in
@@ -356,8 +358,8 @@ let make_case_or_project env sigma indf ci pred c branches =
   | None -> (mkCase (ci, pred, c, branches))
   | Some ps ->
      assert(Array.length branches == 1);
+     let na, ty, t = destLambda sigma pred in
      let () =
-       let _, _, t = destLambda sigma pred in
        let (ind, _), _ = dest_ind_family indf in
        let mib, _ = Inductive.lookup_mind_specif env ind in
        if (* dependent *) not (Vars.noccurn sigma 1 t) &&
@@ -368,16 +370,18 @@ let make_case_or_project env sigma indf ci pred c branches =
      in
      let branch = branches.(0) in
      let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
-     let n, subst =
+     let n, len, ctx =
        List.fold_right
-         (fun decl (i, subst) ->
+         (fun decl (i, j, ctx) ->
           match decl with
-          | LocalAssum (na, t) ->
-             let t = mkProj (Projection.make ps.(i) true, c) in
-             (i + 1, t :: subst)
-          | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
-         ctx (0, [])
-     in Vars.substl subst br
+          | LocalAssum (na, ty) ->
+             let t = mkProj (Projection.make ps.(i) true, mkRel j) in
+             (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx)
+          | LocalDef (na, b, ty) ->
+             (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx))
+         ctx (0, 1, [])
+     in
+     mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx)
 
 (* substitution in a signature *)
 
@@ -454,6 +458,110 @@ let build_branch_type env sigma dep p cs =
 
 (**************************************************)
 
+(** From a rel context describing the constructor arguments,
+    build an expansion function.
+    The term built is expecting to be substituted first by
+    a substitution of the form [params, x : ind params] *)
+let compute_projections env (kn, i as ind) =
+  let open Term in
+  let mib = Environ.lookup_mind kn env in
+  let indu = match mib.mind_universes with
+  | Monomorphic_ind _ -> mkInd ind
+  | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx)
+  | Cumulative_ind ctx ->
+    mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
+  in
+  let x = match mib.mind_record with
+  | NotRecord | FakeRecord ->
+    anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+  | PrimRecord info-> Name (pi1 (info.(i)))
+  in
+  (** FIXME: handle mutual records *)
+  let pkt = mib.mind_packets.(0) in
+  let { mind_consnrealargs; mind_consnrealdecls } = pkt in
+  let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
+  let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in
+  let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
+  let mp, dp, l = MutInd.repr3 kn in
+  (** We build a substitution smashing the lets in the record parameters so
+      that typechecking projections requires just a substitution and not
+      matching with a parameter context. *)
+  let indty =
+    (* [ty] = [Ind inst] is typed in context [params] *)
+    let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+    let ty = mkApp (indu, inst) in
+    (* [Ind inst] is typed in context [params-wo-let] *)
+    ty
+  in
+  let ci =
+    let print_info =
+      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+      { ci_ind     = ind;
+        ci_npar    = nparamargs;
+        ci_cstr_ndecls = mind_consnrealdecls;
+        ci_cstr_nargs = mind_consnrealargs;
+        ci_pp_info = print_info }
+  in
+  let len = List.length ctx in
+  let compat_body ccl i =
+    (* [ccl] is defined in context [params;x:indty] *)
+    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
+    let ccl' = liftn 1 2 ccl in
+    let p = mkLambda (x, lift 1 indty, ccl') in
+    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
+    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
+      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
+  in
+  let projections decl (j, pbs, subst) =
+    match decl with
+    | LocalDef (na,c,t) ->
+        (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
+        let c = liftn 1 j c in
+        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
+        let c1 = substl subst c in
+        (* From [params, x:I |- subst:field1,..,fieldj]
+           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
+           is represented with instance of field1 last *)
+        let subst = c1 :: subst in
+        (j+1, pbs, subst)
+    | LocalAssum (na,t) ->
+      match na with
+      | Name id ->
+        let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+        (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
+        let t = liftn 1 j t in
+        (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
+        (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
+           to [params, x:I |- t(proj1 x,..,projj x)] *)
+        let ty = substl subst t in
+        let term = mkProj (Projection.make kn true, mkRel 1) in
+        let fterm = mkProj (Projection.make kn false, mkRel 1) in
+        let compat = compat_body ty (j - 1) in
+        let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+        let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
+        let body = (etab, etat, compat) in
+        (j + 1, body :: pbs, fterm :: subst)
+      | Anonymous ->
+        anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+  in
+  let (_, pbs, subst) =
+    List.fold_right projections ctx (1, [], [])
+  in
+  Array.rev_of_list pbs
+
+let legacy_match_projection env ind =
+  Array.map pi3 (compute_projections env ind)
+
+let compute_projections ind mib =
+  let ans = compute_projections ind mib in
+  Array.map (fun (prj, ty, _) -> (prj, ty)) ans
+
+(**************************************************)
+
 let extract_mrectype sigma t =
   let open EConstr in
   let (t, l) = decompose_app sigma t in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b0d714b03..aa53f7e67 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,6 +194,18 @@ val make_case_or_project :
 val make_default_case_info : env -> case_style -> inductive -> case_info
 i*)
 
+val compute_projections : Environ.env -> inductive -> (constr * types) array
+(** Given a primitive record type, for every field computes the eta-expanded
+    projection and its type. *)
+
+val legacy_match_projection : Environ.env -> inductive -> constr array
+(** Given a record type, computes the legacy match-based projection of the
+    projections.
+
+    BEWARE: such terms are ill-typed, and should thus only be used in upper
+    layers. The kernel will probably badly fail if presented with one of
+    those. *)
+
 (********************)
 
 val type_of_inductive_knowing_conclusion :
diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 95a2e495b..37dd120c1 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -9,10 +9,13 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 
 (** Locus : positions in hypotheses and goals *)
 
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of lident
+
 (** {6 Occurrences} *)
 
 type 'a occurrences_gen =
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 1664e68f2..6b6a3f8a9 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -86,8 +86,8 @@ let concrete_clause_of enum_hyps cl =
 (** Miscellaneous functions *)
 
 let out_arg = function
-  | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
-  | Misctypes.ArgArg x -> x
+  | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
+  | ArgArg x -> x
 
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
deleted file mode 100644
index 1697e54ab..000000000
--- a/pretyping/miscops.ml
+++ /dev/null
@@ -1,55 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Misctypes
-
-(** Mapping [cast_type] *)
-
-let map_cast_type f = function
-  | CastConv a -> CastConv (f a)
-  | CastVM a -> CastVM (f a)
-  | CastCoerce -> CastCoerce
-  | CastNative a -> CastNative (f a)
-
-let smartmap_cast_type f c =
-  match c with
-    | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
-    | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
-    | CastCoerce -> CastCoerce
-    | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
-
-(** Equalities on [glob_sort] *)
-
-let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
-| GProp, GProp -> true
-| GSet, GSet -> true
-| GType l1, GType l2 ->
-   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
-| _ -> false
-
-let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
-| IntroAnonymous, IntroAnonymous -> true
-| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
-| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
-| _ -> false
-
-(** Mapping bindings *)
-
-let map_explicit_bindings f l =
-  let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in
-  List.map map l
-
-let map_bindings f = function
-| ImplicitBindings l -> ImplicitBindings (List.map f l)
-| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl)
-| NoBindings -> NoBindings
-
-let map_with_bindings f (x, bl) = (f x, map_bindings f bl)
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
deleted file mode 100644
index 6a84fb9eb..000000000
--- a/pretyping/miscops.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Misctypes
-
-(** Mapping [cast_type] *)
-
-val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
-val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
-
-(** Equalities on [glob_sort] *)
-
-val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
-
-(** Equalities on [intro_pattern_naming] *)
-
-val intro_pattern_naming_eq :
-  intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
-
-(** Mapping bindings *)
-
-val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
-val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 4b8e0e096..7319846fb 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -188,12 +188,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 get_proj env ((mind, n), i) =
   let mib = Environ.lookup_mind mind env in
   match mib.mind_record with
-  | None | Some None ->
+  | NotRecord | FakeRecord ->
     CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
-  | Some (Some (_, projs, _)) ->
+  | PrimRecord info ->
+    let _, projs, _ = info.(n) in
     Projection.make projs.(i) true
 
 let rec nf_val env sigma v typ =
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 996a2dc36..be7ebe49c 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -9,10 +9,12 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 
 (** {5 Patterns} *)
 
+(** Cases pattern variables *)
+type patvar = Id.t
+
 type case_info_pattern =
     { cip_style : Constr.case_style;
       cip_ind : inductive option;
@@ -22,7 +24,7 @@ type case_info_pattern =
 type constr_pattern =
   | PRef of GlobRef.t
   | PVar of Id.t
-  | PEvar of existential_key * constr_pattern array
+  | PEvar of Evar.t * constr_pattern array
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of patvar * constr_pattern list
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 9342b4cc7..622a8e982 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -18,7 +18,6 @@ open Constr
 open Glob_term
 open Pp
 open Mod_subst
-open Misctypes
 open Decl_kinds
 open Pattern
 open Environ
@@ -47,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
   Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
   Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
-| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2
 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
@@ -418,7 +417,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
       let mkGLambda na c = DAst.make ?loc @@
-	GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+        GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in
       let c = List.fold_right mkGLambda nal c in
       let cip =
 	{ cip_style = LetStyle;
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index dfbfb147f..36317b3ac 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Mod_subst
-open Misctypes
 open Glob_term
 open Pattern
 open EConstr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b2507b5f2..57c4d363b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,7 +45,6 @@ open Pretype_errors
 open Glob_term
 open Glob_ops
 open Evarconv
-open Misctypes
 open Ltac_pretype
 
 module NamedDecl = Context.Named.Declaration
@@ -172,38 +171,37 @@ let _ =
 
 (** Miscellaneous interpretation functions *)
 
-let interp_known_universe_level evd r =
-  let qid = Libnames.qualid_of_reference r in
+let interp_known_universe_level evd qid =
   try
-    match r.CAst.v with
-    | Libnames.Ident id -> Evd.universe_of_name evd id
-    | Libnames.Qualid _ -> raise Not_found
+    let open Libnames in
+    if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
+    else raise Not_found
   with Not_found ->
-    let univ, k = Nametab.locate_universe qid.CAst.v in
+    let univ, k = Nametab.locate_universe qid in
     Univ.Level.make univ k
 
-let interp_universe_level_name ~anon_rigidity evd r =
-  try evd, interp_known_universe_level evd r
+let interp_universe_level_name ~anon_rigidity evd qid =
+  try evd, interp_known_universe_level evd qid
   with Not_found ->
-    match r with (* Qualified generated name *)
-    | {CAst.loc; v=Libnames.Qualid qid} ->
-       let dp, i = Libnames.repr_qualid qid in
-       let num =
-         try int_of_string (Id.to_string i)
-         with Failure _ ->
-           user_err ?loc ~hdr:"interp_universe_level_name"
-                    (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r))
-       in
-       let level = Univ.Level.make dp num in
-       let evd =
-         try Evd.add_global_univ evd level
-         with UGraph.AlreadyDeclared -> evd
-       in evd, level
-    | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *)
-        if not (is_strict_universe_declarations ()) then
-          new_univ_level_variable ?loc ~name:id univ_rigid evd
-        else user_err ?loc ~hdr:"interp_universe_level_name"
-                      (Pp.(str "Undeclared universe: " ++ Id.print id))
+    if Libnames.qualid_is_ident qid then (* Undeclared *)
+      let id = Libnames.qualid_basename qid in
+      if not (is_strict_universe_declarations ()) then
+        new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
+      else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+          (Pp.(str "Undeclared universe: " ++ Id.print id))
+    else
+      let dp, i = Libnames.repr_qualid qid in
+      let num =
+        try int_of_string (Id.to_string i)
+        with Failure _ ->
+          user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+            (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
+      in
+      let level = Univ.Level.make dp num in
+      let evd =
+        try Evd.add_global_univ evd level
+        with UGraph.AlreadyDeclared -> evd
+      in evd, level
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
@@ -233,10 +231,10 @@ let interp_known_level_info ?loc evd = function
   | UUnknown | UAnonymous ->
     user_err ?loc ~hdr:"interp_known_level_info"
       (str "Anonymous universes not allowed here.")
-  | UNamed ref ->
-    try interp_known_universe_level evd ref
+  | UNamed qid ->
+    try interp_known_universe_level evd qid
     with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
+      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
 
 let interp_level_info ?loc evd : level_info -> _ = function
   | UUnknown -> new_univ_level_variable ?loc univ_rigid evd
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 70588b6ad..d3aa7ac64 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,7 +30,7 @@ type 'a hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
 
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 
 let typeclasses_unique_solutions = ref false
 let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c78382c82..e4a56960c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -21,7 +21,7 @@ type 'a hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
 
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 
 (** This module defines type-classes *)
 type typeclass = {
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index a1ac53c73..2720a3e4d 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -18,7 +18,7 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
     | NotAClass of constr
-    | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
+    | UnboundMethod of GlobRef.t * lident (* Class name, method *)
 
 exception TypeClassError of env * typeclass_error
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 1003f2ae1..9831627a9 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -16,11 +16,11 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
   | NotAClass of constr
-  | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
+  | UnboundMethod of GlobRef.t * lident (** Class name, method *)
 
 exception TypeClassError of env * typeclass_error
 
 val not_a_class : env -> constr -> 'a
 
-val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
+val unbound_method : env -> GlobRef.t -> lident -> 'a
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bffe36eea..cf34ac016 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -197,10 +197,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
-  let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
+  let pj = Retyping.get_judgment_of env sigma p in
+  let _, s = splay_prod env sigma pj.uj_type in
+  let ksort = match EConstr.kind sigma s with
+  | Sort s -> Sorts.family (ESorts.kind sigma s)
+  | _ -> error_elim_arity env sigma ind sorts c pj None in
   if not (List.exists ((==) ksort) sorts) then
     let s = inductive_sort_family (snd specif) in
     error_elim_arity env sigma ind sorts c pj
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5cf6e4b26..4ba5d2794 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t =
 
 let is_eta_constructor_app env sigma ts f l1 term =
   match EConstr.kind sigma f with
-  | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
+  | Construct (((_, i as ind), j), u) when j == 1 ->
+    let open Declarations in
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
+      | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite &&
+          let (_, projs, _) = info.(i) in
           Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
 	(** Check that the other term is neutral *)
 	is_neutral env sigma ts term
@@ -667,11 +669,13 @@ 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
-      | Some (Some (_, projs, _)) ->
+      | PrimRecord info ->
+        let (_, projs, _) = info.(i) in
         let npars = mib.Declarations.mind_nparams in
 	let pars, l1' = Array.chop npars l1 in
 	let arg = Array.append pars [|term|] in