Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.

42 files changed, 257 insertions, 165 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 166340b41..28e9ffdb2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -23,12 +23,21 @@ val make : Sorts.t -> t
 val kind : Evd.evar_map -> t -> Sorts.t
 val unsafe_to_sorts : t -> Sorts.t
 end
+module EInstance :
+sig
+type t
+val make : Univ.Instance.t -> t
+val kind : Evd.evar_map -> t -> Univ.Instance.t
+val empty : t
+val is_empty : t -> bool
+val unsafe_to_instance : t -> Univ.Instance.t
+end
 type t
-val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
 val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
@@ -50,6 +59,16 @@ struct
   let unsafe_to_sorts s = s
 end
 
+module EInstance =
+struct
+  type t = Univ.Instance.t
+  let make i = i
+  let kind sigma i = Evd.normalize_universe_instance sigma i
+  let empty = Univ.Instance.empty
+  let is_empty = Univ.Instance.is_empty
+  let unsafe_to_instance t = t
+end
+
 type t = Constr.t
 
 let safe_evar_value sigma ev =
@@ -63,15 +82,6 @@ let rec whd_evar sigma c =
     | Some c -> whd_evar sigma c
     | None -> c
     end
-  | Const (c', u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkConstU (c', u')
-  | Ind (i, u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkIndU (i, u')
-  | Construct (co, u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkConstructU (co, u')
   | App (f, args) when isEvar f ->
     (** Enforce smart constructor invariant on applications *)
     let ev = destEvar f in
@@ -137,7 +147,7 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt
 type named_context = (constr, types) Context.Named.pt
 type rel_context = (constr, types) Context.Rel.pt
 
-let in_punivs a = (a, Univ.Instance.empty)
+let in_punivs a = (a, EInstance.empty)
 
 let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
 let mkSet = of_kind (Sort (ESorts.make Sorts.set))
@@ -762,6 +772,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
 module Unsafe =
 struct
 let to_sorts = ESorts.unsafe_to_sorts
+let to_instance = EInstance.unsafe_to_instance
 let to_constr = unsafe_to_constr
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index db10fbf42..3a9469e55 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -45,9 +45,21 @@ sig
 
 end
 
+module EInstance :
+sig
+  type t
+  (** Type of universe instances up-to universe unification. Similar to
+      {ESorts.t} for {Univ.Instance.t}. *)
+
+  val make : Univ.Instance.t -> t
+  val kind : Evd.evar_map -> t -> Univ.Instance.t
+  val empty : t
+  val is_empty : t -> bool
+end
+
 (** {5 Destructors} *)
 
-val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
 (** Same as {!Constr.kind} except that it expands evars and normalizes
     universes on the fly. *)
 
@@ -60,7 +72,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
 (** {5 Constructors} *)
 
-val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
 (** Construct a term from a view. *)
 
 val of_constr : Constr.t -> t
@@ -89,13 +101,13 @@ val mkLambda : Name.t * t * t -> t
 val mkLetIn : Name.t * t * t * t -> t
 val mkApp : t * t array -> t
 val mkConst : constant -> t
-val mkConstU : pconstant -> t
+val mkConstU : constant * EInstance.t -> t
 val mkProj : (projection * t) -> t
 val mkInd : inductive -> t
-val mkIndU : pinductive -> t
+val mkIndU : inductive * EInstance.t -> t
 val mkConstruct : constructor -> t
-val mkConstructU : pconstructor -> t
-val mkConstructUi : pinductive * int -> t
+val mkConstructU : constructor * EInstance.t -> t
+val mkConstructUi : (inductive * EInstance.t) * int -> t
 val mkCase : case_info * t * t * t array -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
@@ -146,10 +158,10 @@ val destProd : Evd.evar_map -> t -> Name.t * types * types
 val destLambda : Evd.evar_map -> t -> Name.t * types * t
 val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
 val destApp : Evd.evar_map -> t -> t * t array
-val destConst : Evd.evar_map -> t -> constant puniverses
+val destConst : Evd.evar_map -> t -> constant * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
-val destInd : Evd.evar_map -> t -> inductive puniverses
-val destConstruct : Evd.evar_map -> t -> constructor puniverses
+val destInd : Evd.evar_map -> t -> inductive * EInstance.t
+val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
 val destCase : Evd.evar_map -> t -> case_info * t * t * t array
 val destProj : Evd.evar_map -> t -> projection * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
@@ -262,6 +274,9 @@ sig
   val to_sorts : ESorts.t -> Sorts.t
   (** Physical identity. Does not care for normalization. *)
 
+  val to_instance : EInstance.t -> Univ.Instance.t
+  (** Physical identity. Does not care for normalization. *)
+
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)
 end
diff --git a/engine/termops.ml b/engine/termops.ml
index a67916345..64f4c6dc5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1150,7 +1150,7 @@ let global_of_constr sigma c =
   | Const (c, u) -> ConstRef c, u
   | Ind (i, u) -> IndRef i, u
   | Construct (c, u) -> ConstructRef c, u
-  | Var id -> VarRef id, Univ.Instance.empty
+  | Var id -> VarRef id, EConstr.EInstance.empty
   | _ -> raise Not_found
 
 let is_global sigma c t =
@@ -1169,8 +1169,12 @@ let isGlobalRef sigma c =
 
 let is_template_polymorphic env sigma f =
   match EConstr.kind sigma f with
-  | Ind ind -> Environ.template_polymorphic_pind ind env
-  | Const c -> Environ.template_polymorphic_pconstant c env
+  | Ind (ind, u) ->
+    if not (EConstr.EInstance.is_empty u) then false
+    else Environ.template_polymorphic_ind ind env
+  | Const (cst, u) ->
+    if not (EConstr.EInstance.is_empty u) then false
+    else Environ.template_polymorphic_constant cst env
   | _ -> false
 
 let base_sort_cmp pb s0 s1 =
@@ -1453,8 +1457,8 @@ let global_app_of_constr sigma c =
   | Const (c, u) -> (ConstRef c, u), None
   | Ind (i, u) -> (IndRef i, u), None
   | Construct (c, u) -> (ConstructRef c, u), None
-  | Var id -> (VarRef id, Instance.empty), None
-  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
+  | Var id -> (VarRef id, EConstr.EInstance.empty), None
+  | Proj (p, c) -> (ConstRef (Projection.constant p), EConstr.EInstance.empty), Some c
   | _ -> raise Not_found
 
 let prod_applist sigma c l =
diff --git a/engine/termops.mli b/engine/termops.mli
index 0dd5d96fb..fe6dfb0ce 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -250,7 +250,7 @@ val clear_named_body : Id.t -> env -> env
 val global_vars : env -> Evd.evar_map -> constr -> Id.t list
 val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t
 val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t
-val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option
+val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
@@ -259,7 +259,7 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
 
-val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses
+val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t
 
 val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c9c904e35..2d9dec095 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -66,6 +66,7 @@ let rec decompose_term env sigma t=
 	      decompose_term env sigma b)
     | Construct c ->
 	let (((mind,i_ind),i_con),u)= c in 
+	let u = EInstance.kind sigma u in
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
@@ -75,9 +76,11 @@ let rec decompose_term env sigma t=
 		       ci_nhyps=nargs-oib.mind_nparams}
     | Ind c -> 
 	let (mind,i_ind),u = c in 
+	let u = EInstance.kind sigma u in
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
     | Const (c,u) -> 
+	let u = EInstance.kind sigma u in
 	let canon_const = constant_of_kn (canonical_con c) in 
 	  (Symb (Constr.mkConstU (canon_const,u)))
     | Proj (p, c) -> 
@@ -408,7 +411,8 @@ let build_term_to_complete uf meta pac =
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
   let dummy_args = List.rev (List.init pac.arity meta) in
   let all_args = List.rev_append real_args dummy_args in
-    applist (mkConstructU cinfo.ci_constr, all_args)
+  let (kn, u) = cinfo.ci_constr in
+    applist (mkConstructU (kn, EInstance.make u), all_args)
 
 let cc_tactic depth additionnal_terms =
   Proofview.Goal.enter { enter = begin fun gl ->
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 87bac2fe3..7773f6a2f 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -91,6 +91,7 @@ let kind_of_formula gl term =
 		  Some (i,l,n)->
                     let l = List.map EConstr.Unsafe.to_constr l in
 		    let ind,u=EConstr.destInd (project gl) i in
+		    let u = EConstr.EInstance.kind (project gl) u in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
 		      if Int.equal nconstr 0 then
@@ -112,7 +113,10 @@ let kind_of_formula gl term =
 			      Or((ind,u),l,is_trivial)
 		| _ ->
 		    match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with
-			Some (i,l)-> Exists((EConstr.destInd (project gl) i),List.map EConstr.Unsafe.to_constr l)
+			Some (i,l)->
+                          let (ind, u) = EConstr.destInd (project gl) i in
+                          let u = EConstr.EInstance.kind (project gl) u in
+                          Exists((ind, u), List.map EConstr.Unsafe.to_constr l)
 		      |_-> Atom (normalize cciterm)
 
 type atoms = {positive:constr list;negative:constr list}
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e845db3bc..529b91c4c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -300,7 +300,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
       hook
   ;
     (*       let _tim1 = System.get_time ()  in *)
-      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map EConstr.mkConstU funs) mutr_nparams)));
+      let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
+      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)));
     (*       let _tim2 =  System.get_time ()  in *)
     (* 	begin *)
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 63bd3848f..8aab3b742 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1275,8 +1275,9 @@ let do_build_inductive
   let open Context.Named.Declaration in
   let evd,env =
     Array.fold_right2
-      (fun id c (evd,env) ->
-       let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in
+      (fun id (c, u) (evd,env) ->
+       let u = EConstr.EInstance.make u in
+       let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
        let t = EConstr.Unsafe.to_constr t in
        evd,
        Environ.push_named (LocalAssum (id,t))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a7489fb7b..2852152e1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -249,7 +249,8 @@ let derive_inversion fix_names =
 	   Evd.fresh_global
 	     (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in 
         let c = EConstr.of_constr c in
-	 evd, destConst evd c::l
+        let (cst, u) = destConst evd c in
+	 evd, (cst, EInstance.kind evd u) :: l
 	)
 	fix_names
 	(evd',[])
@@ -412,7 +413,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
             let c = EConstr.of_constr c in
-	    evd,((destConst evd c)::l)
+            let (cst, u) = destConst evd c in
+            let u = EInstance.kind evd u in
+            evd,((cst, u) :: l)
 	   )
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
@@ -427,7 +430,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
             let c = EConstr.of_constr c in
-	    evd,((destConst evd c)::l)
+            let (cst, u) = destConst evd c in
+            let u = EInstance.kind evd u in
+            evd,((cst, u) :: l)
 	   )
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2c2cd919b..94ec0a898 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -783,7 +783,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
   assert (funs <> []);
   assert (graphs <> []);
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
-  let funs_constr = Array.map mkConstU funs  in
+  let map (c, u) = mkConstU (c, EInstance.make u) in
+  let funs_constr = Array.map map funs  in
   States.with_state_protection_on_exception
     (fun () ->
      let env = Global.env () in
@@ -882,7 +883,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
 	   (Array.to_list
 	      (Array.mapi
-		 (fun i _ -> ((kn,i),u(* Univ.Instance.empty *)),true,InType)
+		 (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType)
 		 mib.Declarations.mind_packets
 	      )
 	   )
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 44aacaf45..c0298d06c 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -136,13 +136,14 @@ let prNamedRLDecl s lc =
 
 let showind (id:Id.t) =
   let cstrid = Constrintern.global_reference id in
-  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
-  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
+  let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
+  let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
+  let u = EConstr.Unsafe.to_instance u in
   List.iter (fun decl ->
     print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
     prconstr (RelDecl.get_type decl); print_string "\n")
     ib1.mind_arity_ctxt;
-    Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1);
+    Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u));
   Array.iteri
     (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
     ib1.mind_user_lc
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0a288c76e..5460d6fb7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -86,9 +86,10 @@ let def_of_const t =
 
 let type_of_const sigma t =
    match (EConstr.kind sigma t) with
-   | Const sp ->
+   | Const (sp, u) ->
+      let u = EInstance.kind sigma u in
       (* FIXME discarding universe constraints *)
-      Typeops.type_of_constant_in (Global.env()) sp
+      Typeops.type_of_constant_in (Global.env()) (sp, u)
     |_ -> assert false
 
 let constr_of_global x = 
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 55108631b..b34afd51b 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1073,7 +1073,7 @@ let decompose l c =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let to_ind c =
-      if isInd sigma c then Univ.out_punivs (destInd sigma c)
+      if isInd sigma c then fst (destInd sigma c)
       else error "not an inductive type"
     in
     let l = List.map to_ind l in
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 95620b374..b76009c99 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -255,7 +255,7 @@ let coerce_to_evaluable_ref env sigma v =
     | IndRef _ | ConstructRef _ -> fail ()
   else
     match Value.to_constr v with
-    | Some c when isConst sigma c -> EvalConstRef (Univ.out_punivs (destConst sigma c))
+    | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
     | Some c when isVar sigma c -> EvalVarRef (destVar sigma c)
     | _ -> fail ()
   in if Tacred.is_evaluable env ev then ev else fail ()
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 23069a9ab..fc9d70ae7 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -225,8 +225,9 @@ let compute_rhs env sigma bodyi index_of_f =
 let compute_ivs f cs gl =
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
-  let cst = try destConst sigma f with DestKO -> i_can't_do_that () in
-  let body = Environ.constant_value_in (Global.env()) cst in
+  let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in
+  let u = EInstance.kind sigma u in
+  let body = Environ.constant_value_in (Global.env()) (cst, u) in
   let body = EConstr.of_constr body in
   match decomp_term sigma body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 38c105666..c5cf74ccf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -279,6 +279,7 @@ let rec find_row_ind = function
 let inductive_template evdref env tmloc ind =
   let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in
   let arsign = inductive_alldecls_env env indu in
+  let indu = on_snd EInstance.make indu in
   let hole_source i = match tmloc with
     | Some loc -> (loc, Evar_kinds.TomatchTypeParameter (ind,i))
     | None -> (Loc.ghost, Evar_kinds.TomatchTypeParameter (ind,i)) in
@@ -1314,7 +1315,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
       let cur_alias = lift const_info.cs_nargs current in
       let ind =
         mkApp (
-          applist (mkIndU (inductive_of_constructor (fst const_info.cs_cstr), snd const_info.cs_cstr),
+          applist (mkIndU (inductive_of_constructor (fst const_info.cs_cstr), EInstance.make (snd const_info.cs_cstr)),
                    List.map (EConstr.of_constr %> lift const_info.cs_nargs) const_info.cs_params),
           Array.map EConstr.of_constr const_info.cs_concl_realargs) in
       Alias (initial,(aliasname,cur_alias,(ci,ind))) in
@@ -2104,7 +2105,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	let args = List.rev args in
 	let patargs = List.rev patargs in
 	let pat' = PatCstr (l, cstr, patargs, alias) in
-	let cstr = mkConstructU ci.cs_cstr in
+	let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in
 	let app = applist (cstr, List.map (lift (List.length sign)) params) in
 	let app = applist (app, args) in
 	let apptype = Retyping.get_type_of env ( !evdref) app in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 13310c44d..632ba0d9c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -193,15 +193,16 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab
 (* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *)
 
 let find_class_type sigma t =
+  let open EConstr in
   let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
   match EConstr.kind sigma t' with
-    | Var id -> CL_SECVAR id, Univ.Instance.empty, args
+    | 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), Univ.Instance.empty, (c :: args)
+      CL_PROJ (Projection.constant p), EInstance.empty, (c :: args)
     | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
-    | Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, []
-    | Sort _ -> CL_SORT, Univ.Instance.empty, []
+    | Prod (_,_,_) -> CL_FUN, EInstance.empty, []
+    | Sort _ -> CL_SORT, EInstance.empty, []
     |  _ -> raise Not_found
 
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index a1d030f12..0d741a5a5 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -60,7 +60,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 
 (** [find_class_type env sigma c] returns the head reference of [c],
     its universe instance and its arguments *)
-val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list
+val find_class_type : evar_map -> types -> cl_typ * EInstance.t * constr list
 
 (** raises [Not_found] if not convertible to a class *)
 val class_of : env -> evar_map -> types -> types * cl_index
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 84022f57f..e4d7ab38d 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -438,6 +438,7 @@ let detype_level sigma l =
   GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
 
 let detype_instance sigma l = 
+  let l = EInstance.kind sigma l in
   if Univ.Instance.is_empty l then None
   else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
@@ -507,6 +508,7 @@ let rec detype flags avoid env sigma t =
 	      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
+	      let u = EInstance.kind sigma u in
 	      let body' = CVars.subst_instance_constr u body' in
 	      let body' = EConstr.of_constr body' in
 		substl (c :: List.rev args) body'
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b6fa25769..9c9350ab1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -51,9 +51,9 @@ let unfold_projection env evd ts p c =
       
 let eval_flexible_term ts env evd c =
   match EConstr.kind evd c with
-  | Const (c,u as cu) ->
+  | Const (c, u) ->
       if is_transparent_constant ts c
-      then Option.map EConstr.of_constr (constant_opt_value_in env cu)
+      then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u))
       else None
   | Rel n ->
       (try match lookup_rel n env with
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 88c492f03..5b42add28 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -74,6 +74,7 @@ let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n)
 
 let mkAppliedInd (IndType ((ind,params), realargs)) =
   let open EConstr in
+  let ind = on_snd EInstance.make ind in
   applist (mkIndU ind, (List.map EConstr.of_constr params)@realargs)
 
 (* Does not consider imbricated or mutually recursive types *)
@@ -471,11 +472,12 @@ let find_rectype env sigma c =
   let open EConstr in
   let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
-    | Ind (ind,u as indu) ->
+    | Ind (ind,u) ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
         if mib.mind_nparams > List.length l then raise Not_found;
         let l = List.map EConstr.Unsafe.to_constr l in
         let (par,rargs) = List.chop mib.mind_nparams l in
+        let indu = (ind, EInstance.kind sigma u) in
         IndType((indu, par),List.map EConstr.of_constr rargs)
     | _ -> raise Not_found
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index ab470a540..bdb6f996b 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -161,12 +161,12 @@ val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr
 val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types
 
 (** Raise [Not_found] if not given a valid inductive type *)
-val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list
-val find_mrectype    : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list
-val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr array
+val extract_mrectype : evar_map -> EConstr.t -> (inductive * EConstr.EInstance.t) * EConstr.constr list
+val find_mrectype    : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * EConstr.constr list
+val find_mrectype_vect : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * EConstr.constr array
 val find_rectype     : env -> evar_map -> EConstr.types -> inductive_type
-val find_inductive   : env -> evar_map -> EConstr.types -> pinductive * constr list
-val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list
+val find_inductive   : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * constr list
+val find_coinductive : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * constr list
 
 (********************)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8be3b8328..270320538 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -550,7 +550,7 @@ struct
 
   let constr_of_cst_member f sk =
     match f with
-    | Cst_const (c, u) -> mkConstU (c,u), sk
+    | Cst_const (c, u) -> mkConstU (c, EInstance.make u), sk
     | Cst_proj p -> 
       match decomp sk with
       | Some (hd, sk) -> mkProj (p, hd), sk
@@ -703,7 +703,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
             csts Univ.LMap.empty
           in
           let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
-          mkConstU (cst,inst)
+          mkConstU (cst, EInstance.make inst)
         | None -> bd
         end
     with
@@ -856,7 +856,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       | Some body -> whrec cst_l (EConstr.of_constr body, stack)
       | None -> fold ())
     | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) ->
-       (match constant_opt_value_in env const with
+        let u' = EInstance.kind sigma u in
+       (match constant_opt_value_in env (fst const, u') with
 	| None -> fold ()
 	| Some body ->
           let body = EConstr.of_constr body in
@@ -895,7 +896,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 		    | None -> fold ()
 		    | Some (bef,arg,s') ->
 		      whrec Cst_stack.empty 
-			(arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s')
+			(arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
        )
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
       (let pb = lookup_projection p env in
@@ -998,6 +999,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	      (match constant_opt_value_in env const with
 	      | None -> fold ()
 	      | Some body ->
+                let const = (fst const, EInstance.make (snd const)) in
                 let body = EConstr.of_constr body in
 		whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
 		  (body, s' @ (Stack.append_app [|x'|] s'')))
@@ -1657,12 +1659,13 @@ let meta_reducible_instance evd b =
 
 
 let head_unfold_under_prod ts env sigma c =
-  let unfold (cst,u as cstu) =
+  let unfold (cst,u) =
+    let cstu = (cst, EInstance.kind sigma u) in
     if Cpred.mem cst (snd ts) then
       match constant_opt_value_in env cstu with
 	| Some c -> EConstr.of_constr c
-	| None -> mkConstU cstu
-    else mkConstU cstu in
+	| None -> mkConstU (cst, u)
+    else mkConstU (cst, u) in
   let rec aux c =
     match EConstr.kind sigma c with
       | Prod (n,t,c) -> mkProd (n,aux t, aux c)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 01707b47a..752c30a8a 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -232,7 +232,7 @@ type 'a miota_args = {
 val reducible_mind_case : evar_map -> constr -> bool
 val reduce_mind_case : evar_map -> constr miota_args -> constr
 
-val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, Univ.Instance.t) kind_of_term
+val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term
 val is_arity : env ->  evar_map -> constr -> bool
 val is_sort : env -> evar_map -> types -> bool
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 9c9751af8..496c706ec 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -102,10 +102,10 @@ let retype ?(polyprop=true) sigma =
 	let ty = RelDecl.get_type (lookup_rel n env) in
         lift n ty
     | Var id -> type_of_var env id
-    | Const cst -> EConstr.of_constr (rename_type_of_constant env cst)
+    | Const (cst, u) -> EConstr.of_constr (rename_type_of_constant env (cst, EInstance.kind sigma u))
     | Evar ev -> existential_type sigma ev
-    | Ind ind -> EConstr.of_constr (rename_type_of_inductive env ind)
-    | Construct cstr -> EConstr.of_constr (rename_type_of_constructor env cstr)
+    | Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u))
+    | Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u))
     | Case (_,p,c,lf) ->
         let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
@@ -186,16 +186,20 @@ let retype ?(polyprop=true) sigma =
     let argtyps =
       Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in
     match EConstr.kind sigma c with
-    | Ind ind ->
-      let mip = lookup_mind_specif env (fst ind) in
+    | Ind (ind, u) ->
+      let u = EInstance.kind sigma u in
+      let mip = lookup_mind_specif env ind in
 	EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters
-	       ~polyprop env (mip,snd ind) argtyps
+	       ~polyprop env (mip, u) argtyps
 	 with Reduction.NotArity -> retype_error NotAnArity)
-    | Const cst ->
-	EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps
+    | Const (cst, u) ->
+        let u = EInstance.kind sigma u in
+	EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env (cst, u) argtyps
 	 with Reduction.NotArity -> retype_error NotAnArity)
     | Var id -> type_of_var env id
-    | Construct cstr -> EConstr.of_constr (type_of_constructor env cstr)
+    | Construct (cstr, u) ->
+      let u = EInstance.kind sigma u in
+      EConstr.of_constr (type_of_constructor env (cstr, u))
     | _ -> assert false
 
   in type_of, sort_of, sort_family_of,
@@ -212,13 +216,13 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
   match EConstr.kind sigma c with
     | Ind (ind,u) ->
         let spec = Inductive.lookup_mind_specif env ind in
-          type_of_inductive_knowing_conclusion env sigma (spec,u) conclty
-    | Const cst ->
-        let t = constant_type_in env cst in
+          type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty
+    | Const (cst, u) ->
+        let t = constant_type_in env (cst, EInstance.kind sigma u) in
         (* TODO *)
           sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||])
     | Var id -> sigma, type_of_var env id
-    | Construct cstr -> sigma, EConstr.of_constr (type_of_constructor env cstr)
+    | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))
     | _ -> assert false
 
 (* Profiling *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ef9f39d77..67221046b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -60,6 +60,7 @@ let is_evaluable env = function
 let value_of_evaluable_ref env evref u =
   match evref with
   | EvalConstRef con -> 
+    let u = Unsafe.to_instance u in
     EConstr.of_constr (try constant_value_in env (con,u)
     with NotEvaluableConst IsProj -> 
       raise (Invalid_argument "value_of_evaluable_ref"))
@@ -103,9 +104,9 @@ let isEvalRef env sigma c = match EConstr.kind sigma c with
 
 let destEvalRefU sigma c = match EConstr.kind sigma c with
   | Const (cst,u) ->  EvalConst cst, u
-  | Var id  -> (EvalVar id, Univ.Instance.empty)
-  | Rel n -> (EvalRel n, Univ.Instance.empty)
-  | Evar ev -> (EvalEvar ev, Univ.Instance.empty)
+  | Var id  -> (EvalVar id, EInstance.empty)
+  | Rel n -> (EvalRel n, EInstance.empty)
+  | Evar ev -> (EvalEvar ev, EInstance.empty)
   | _ -> anomaly (Pp.str "Not an unfoldable reference")
 
 let unsafe_reference_opt_value env sigma eval =
@@ -125,7 +126,9 @@ let unsafe_reference_opt_value env sigma eval =
 
 let reference_opt_value env sigma eval u = 
   match eval with
-  | EvalConst cst -> Option.map EConstr.of_constr (constant_opt_value_in env (cst,u))
+  | EvalConst cst ->
+    let u = EInstance.kind sigma u in
+    Option.map EConstr.of_constr (constant_opt_value_in env (cst,u))
   | EvalVar id ->
       env |> lookup_named id |> NamedDecl.get_value
   | EvalRel n ->
@@ -519,13 +522,13 @@ let reduce_mind_case_use_function func env sigma mia =
 		       mutual inductive, try to reuse the global name if
 		       the block was indeed initially built as a global
 		       definition *)
-		    let kn = map_puniverses (fun x -> con_with_label x (Label.of_id id))
-		      (destConst sigma func)
-		    in
-		    try match constant_opt_value_in env kn with
+                    let (kn, u) = destConst sigma func in
+                    let kn = con_with_label kn (Label.of_id id) in
+                    let cst = (kn, EInstance.kind sigma u) in
+		    try match constant_opt_value_in env cst with
 		      | None -> None
                           (* TODO: check kn is correct *)
-		      | Some _ -> Some (minargs,mkConstU kn)
+		      | Some _ -> Some (minargs,mkConstU (kn, u))
 		    with Not_found -> None
 	  else
 	    fun _ -> None in
@@ -539,14 +542,15 @@ let match_eval_ref env sigma constr =
   match EConstr.kind sigma constr with
   | Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
       Some (EvalConst sp, u)
-  | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, Univ.Instance.empty)
-  | Rel i -> Some (EvalRel i, Univ.Instance.empty)
-  | Evar ev -> Some (EvalEvar ev, Univ.Instance.empty)
+  | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, EInstance.empty)
+  | Rel i -> Some (EvalRel i, EInstance.empty)
+  | Evar ev -> Some (EvalEvar ev, EInstance.empty)
   | _ -> None
 
 let match_eval_ref_value env sigma constr = 
   match EConstr.kind sigma constr with
   | Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
+    let u = EInstance.kind sigma u in
     Some (EConstr.of_constr (constant_value_in env (sp, u)))
   | Var id when is_evaluable env (EvalVarRef id) -> 
      env |> lookup_named id |> NamedDecl.get_value
@@ -628,8 +632,9 @@ let whd_nothing_for_iota env sigma s =
       | Meta ev ->
 	(try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack)
 	with Not_found -> s)
-      | Const const when is_transparent_constant full_transparent_state (fst const) ->
-	  (match constant_opt_value_in env const with
+      | Const (const, u) when is_transparent_constant full_transparent_state const ->
+          let u = EInstance.kind sigma u in
+	  (match constant_opt_value_in env (const, u) with
 	     | Some  body -> whrec (EConstr.of_constr body, stack)
 	     | None -> s)
       | LetIn (_,b,_,c) -> stacklam whrec [b] sigma c stack
@@ -955,7 +960,7 @@ let simpl env sigma c = strong whd_simpl env sigma c
 let matches_head env sigma c t =
   match EConstr.kind sigma t with
     | App (f,_) -> Constr_matching.matches env sigma c f
-    | Proj (p, _) -> Constr_matching.matches env sigma c (mkConstU (Projection.constant p, Univ.Instance.empty))
+    | Proj (p, _) -> Constr_matching.matches env sigma c (mkConstU (Projection.constant p, EInstance.empty))
     | _ -> raise Constr_matching.PatternMatchingFailure
 
 (** FIXME: Specific function to handle projections: it ignores what happens on the
@@ -1039,7 +1044,7 @@ let contextually byhead occs f env sigma t =
 let match_constr_evaluable_ref sigma c evref = 
   match EConstr.kind sigma c, evref with
   | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u
-  | Var id, EvalVarRef id' when id_eq id id' -> Some Univ.Instance.empty
+  | Var id, EvalVarRef id' when id_eq id id' -> Some EInstance.empty
   | _, _ -> None
 
 let substlin env sigma evalref n (nowhere_except_in,locs) c =
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index a4499015d..76d0bc241 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -76,12 +76,12 @@ val cbv_norm_flags : CClosure.RedFlags.reds ->  reduction_function
 (** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
    with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_atomic_ind : env ->  evar_map -> types -> pinductive * types
+val reduce_to_atomic_ind : env ->  evar_map -> types -> (inductive * EInstance.t) * types
 
 (** [reduce_to_quantified_ind env sigma t] puts [t] in the form
    [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
-val reduce_to_quantified_ind : env ->  evar_map -> types -> pinductive * types
+val reduce_to_quantified_ind : env ->  evar_map -> types -> (inductive * EInstance.t) * types
 
 (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
    [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
@@ -92,7 +92,7 @@ val reduce_to_atomic_ref :
   env ->  evar_map -> global_reference -> types -> types
 
 val find_hnf_rectype : 
-  env ->  evar_map -> types -> pinductive * constr list
+  env ->  evar_map -> types -> (inductive * EInstance.t) * constr list
 
 val contextually : bool -> occurrences * constr_pattern ->
   (patvar_map -> reduction_function) -> reduction_function
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 478499d91..93c71e6ea 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -303,6 +303,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
 	   | Some (Forward, info) ->
 	     let proj = Option.get proj in
 	     let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in
+	     let u = EConstr.EInstance.kind sigma u in
 	     let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
 	       if check && check_instance env sigma (EConstr.of_constr body) then None
 	       else 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 7990b12cd..8d1c0b94c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -61,13 +61,13 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c
 (** These raise a UserError if not a class.
     Caution: the typeclass structures is not instantiated w.r.t. the universe instance.
     This is done separately by typeclass_univ_instance. *)
-val dest_class_app : env -> evar_map -> EConstr.constr -> typeclass puniverses * constr list
+val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list
 
 (** Get the instantiated typeclass structure for a given universe instance. *)
 val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
 
 (** Just return None if not a class *)
-val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * (typeclass puniverses * constr list)) option
+val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
   
 val instance_impl : instance -> global_reference
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index d9d64e7eb..c2a030bcd 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -35,11 +35,13 @@ let meta_type evd mv =
   let ty = Evd.map_fl EConstr.of_constr ty in
   meta_instance evd ty
 
-let constant_type_knowing_parameters env sigma cst jl =
+let constant_type_knowing_parameters env sigma (cst, u) jl =
+  let u = Unsafe.to_instance u in
   let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
-  EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
+  EConstr.of_constr (type_of_constant_knowing_parameters_in env (cst, u) paramstyp)
 
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
+  let u = Unsafe.to_instance u in
   let mspec = lookup_mind_specif env ind in
   let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
   EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
@@ -140,9 +142,10 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
-  let indspec =
+  let ((ind, u), spec) =
     try find_mrectype env !evdref cj.uj_type
     with Not_found -> error_case_not_inductive env !evdref cj in
+  let indspec = ((ind, EInstance.kind !evdref u), spec) in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
   e_check_branch_types env evdref (fst indspec) cj (lfj,bty);
@@ -224,6 +227,7 @@ let judge_of_projection env sigma p cj =
     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);
@@ -262,14 +266,17 @@ let rec execute env evdref cstr =
     | Var id ->
         judge_of_variable env id
 
-    | Const c ->
-        make_judge cstr (EConstr.of_constr (rename_type_of_constant env c))
+    | Const (c, u) ->
+        let u = EInstance.kind !evdref u in
+        make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u)))
 
-    | Ind ind ->
-	make_judge cstr (EConstr.of_constr (rename_type_of_inductive env ind))
+    | Ind (ind, u) ->
+        let u = EInstance.kind !evdref u in
+	make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u)))
 
-    | Construct cstruct ->
-	make_judge cstr (EConstr.of_constr (rename_type_of_constructor env cstruct))
+    | Construct (cstruct, u) ->
+        let u = EInstance.kind !evdref u in
+	make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u)))
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evdref c in
@@ -305,14 +312,14 @@ let rec execute env evdref cstr =
         let jl = execute_array env evdref args in
 	let j =
 	  match EConstr.kind !evdref f with
-	    | Ind ind when Environ.template_polymorphic_pind ind env ->
+	    | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
-		  (inductive_type_knowing_parameters env !evdref ind jl)
-	    | Const cst when Environ.template_polymorphic_pconstant cst env ->
+		  (inductive_type_knowing_parameters env !evdref (ind, u) jl)
+	    | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
-		  (constant_type_knowing_parameters env !evdref cst jl)
+		  (constant_type_knowing_parameters env !evdref (cst, u) jl)
 	    | _ ->
 		execute env evdref f
 	in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 035b0c223..91781a076 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -535,6 +535,7 @@ let key_of env sigma b flags f =
   | Const (cst, u) when is_transparent env (ConstKey cst) &&
       (Cpred.mem cst (snd flags.modulo_delta)
        || Environ.is_projection cst env) ->
+      let u = EInstance.kind sigma u in
       Some (IsKey (ConstKey (cst, u)))
   | Var id when is_transparent env (VarKey id) && 
       Id.Pred.mem id (fst flags.modulo_delta) ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b38a901c2..e6024785d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -505,9 +505,10 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
   let ct = EConstr.of_constr ct in
   let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
-  let indspec =
+  let ((ind, u), spec) =
     try Tacred.find_hnf_rectype env sigma ct
     with Not_found -> anomaly (Pp.str "mk_casegoals") in
+  let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in
   let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 1b05bc7d6..627a8e0e7 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -68,8 +68,8 @@ val pf_whd_all       : goal sigma -> constr -> constr
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
 val pf_nf_betaiota             : goal sigma -> constr -> constr
-val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types
-val pf_reduce_to_atomic_ind     : goal sigma -> types -> pinductive * types
+val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types
+val pf_reduce_to_atomic_ind     : goal sigma -> types -> (inductive * EInstance.t) * types
 val pf_compute                 : goal sigma -> constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
   -> goal sigma -> constr -> constr
@@ -131,7 +131,7 @@ module New : sig
   val pf_last_hyp           : ('a, 'r) Proofview.Goal.t -> named_declaration
 
   val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
-  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
+  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
 
   val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
   val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index e0dff3739..8d1e0e507 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -472,8 +472,9 @@ let unfold_head env sigma (ids, csts) c =
 	(match Environ.named_body id env with
 	| Some b -> true, EConstr.of_constr b
 	| None -> false, c)
-    | Const (cst,u as c) when Cset.mem cst csts ->
-	true, EConstr.of_constr (Environ.constant_value_in env c)
+    | Const (cst, u) when Cset.mem cst csts ->
+        let u = EInstance.kind sigma u in
+	true, EConstr.of_constr (Environ.constant_value_in env (cst, u))
     | App (f, args) ->
 	(match aux f with
 	| true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 53b468bff..7ae7446c8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -746,6 +746,7 @@ let find_positions env sigma t1 t2 =
 	    let _,rargs2 = List.chop nparams args2 in
             let (mib,mip) = lookup_mind_specif env ind1 in
             let params1 = List.map EConstr.Unsafe.to_constr params1 in
+            let u1 = EInstance.kind sigma u1 in
             let ctxt = (get_constructor ((ind1,u1),mib,mip,params1) i1).cs_args in
             let adjust i = CVars.adjust_rel_to_rel_context ctxt (i+1) - 1 in
             List.flatten
@@ -1324,19 +1325,19 @@ let inject_if_homogenous_dependent_pair ty =
         hd2,ar2 = decompose_app_vect sigma t2 in
     if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit;
     if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit;
-    let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
+    let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
     (* Note: should work even if not an inductive type, but the table only *)
     (* knows inductive types *)
-    if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
+    if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let inj2 = EConstr.of_constr inj2 in
-    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
+    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
       [Proofview.tclEFFECTS eff;
@@ -1783,6 +1784,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let select_equation_name decl =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
+        let u = EInstance.kind sigma u in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
@@ -1834,6 +1836,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let test (_,c) =
     try
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+      let u = EInstance.kind sigma u in
       let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 8e4654c02..851554b83 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -144,6 +144,7 @@ let match_with_tuple sigma t =
   let t = match_with_one_constructor sigma None false true t in
   Option.map (fun (hd,l) ->
     let ind = destInd sigma hd in
+    let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
     let (mib,mip) = Global.lookup_pinductive ind in
     let isrec = mis_is_recursive (fst ind,mib,mip) in
     (hd,l,isrec)) t
@@ -200,8 +201,8 @@ let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
 let match_with_empty_type sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
-    | Ind ind ->
-        let (mib,mip) = Global.lookup_pinductive ind in
+    | Ind (ind, _) ->
+        let (mib,mip) = Global.lookup_inductive ind in
         let nconstr = Array.length mip.mind_consnames in
 	if Int.equal nconstr 0 then Some hdapp else None
     | _ ->  None
@@ -214,8 +215,8 @@ let is_empty_type sigma t = op2bool (match_with_empty_type sigma t)
 let match_with_unit_or_eq_type sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
-    | Ind ind  ->
-        let (mib,mip) = Global.lookup_pinductive ind in
+    | Ind (ind , _) ->
+        let (mib,mip) = Global.lookup_inductive ind in
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
         let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
@@ -369,8 +370,8 @@ let is_forall_term sigma c = op2bool (match_with_forall_term sigma c)
 let match_with_nodep_ind sigma t =
   let (hdapp,args) = decompose_app sigma t in
     match EConstr.kind sigma hdapp with
-      | Ind ind  ->
-          let (mib,mip) = Global.lookup_pinductive ind in
+      | Ind (ind, _)  ->
+          let (mib,mip) = Global.lookup_inductive ind in
 	    if Array.length (mib.mind_packets)>1 then None else
 	      let nodep_constr c = has_nodep_prod_after mib.mind_nparams sigma (EConstr.of_constr c) in
 		if Array.for_all nodep_constr mip.mind_nf_lc then
@@ -387,8 +388,8 @@ let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t)
 let match_with_sigma_type sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
-    | Ind ind  ->
-        let (mib,mip) = Global.lookup_pinductive ind in
+    | Ind (ind, _) ->
+        let (mib,mip) = Global.lookup_inductive ind in
           if Int.equal (Array.length (mib.mind_packets)) 1 &&
 	    (Int.equal mip.mind_nrealargs 0) &&
 	    (Int.equal (Array.length mip.mind_consnames)1) &&
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index c46817f50..dd09c3a4d 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -122,19 +122,19 @@ val match_with_equation:
 (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] 
    Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
 val find_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr ->
-      coq_eq_data * Univ.universe_instance * (types * constr * constr)
+      coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
 val find_this_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr ->
-      coq_eq_data * Univ.universe_instance * (types * constr * constr)
+      coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
-val find_eq_data : evar_map -> constr -> coq_eq_data * Univ.universe_instance * equation_kind
+val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_kind
 
 (** Match a term of the form [(existT A P t p)] 
    Returns associated lemmas and [A,P,t,p] *)
 val find_sigma_data_decompose : evar_map -> constr ->
-  coq_sigma_data * (Univ.universe_instance * constr * constr * constr * constr)
+  coq_sigma_data * (EInstance.t * constr * constr * constr * constr)
 
 (** Match a term of the form [{x:A|P}], returns [A] and [P] *)
 val match_sigma : evar_map -> constr -> constr * constr
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a1cd51047..90b7d6581 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -606,6 +606,7 @@ module New = struct
       isrec allnames tac predicate ind (c, t) =
     Proofview.Goal.enter { enter = begin fun gl ->
     let sigma, elim = (mk_elim ind).enter gl in
+    let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (Proofview.Goal.enter { enter = begin fun gl ->
     let indclause = mk_clenv_from gl (c, t) in
@@ -680,17 +681,19 @@ module New = struct
     (sigma, EConstr.of_constr c)
   end }
 
-  let gl_make_case_dep ind = { enter = begin fun gl ->
+  let gl_make_case_dep (ind, u) = { enter = begin fun gl ->
     let sigma = Sigma.Unsafe.of_evar_map (project gl) in
-    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
+    let u = EInstance.kind (project gl) u in
+    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
       (elimination_sort_of_goal gl)
     in
     (Sigma.to_evar_map sigma, EConstr.of_constr r)
   end }
 
-  let gl_make_case_nodep ind = { enter = begin fun gl ->
+  let gl_make_case_nodep (ind, u) = { enter = begin fun gl ->
     let sigma = Sigma.Unsafe.of_evar_map (project gl) in
-    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
+    let u = EInstance.kind (project gl) u in
+    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
       (elimination_sort_of_goal gl)
     in
     (Sigma.to_evar_map sigma, EConstr.of_constr r)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 5839666a7..3b90ec514 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -124,7 +124,7 @@ val fix_empty_or_and_pattern : int ->
   delayed_open_constr or_and_intro_pattern_expr ->
   delayed_open_constr or_and_intro_pattern_expr
 
-val compute_constructor_signatures : rec_flag -> pinductive -> bool list array
+val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array
 
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
@@ -256,11 +256,11 @@ module New : sig
 
   val case_then_using :
     or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    constr option -> pinductive -> constr * types -> unit Proofview.tactic
+    constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
 
   val case_nodep_then_using :
     or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    constr option -> pinductive -> constr * types -> unit Proofview.tactic
+    constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
 
   val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
   val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 55d6df659..8306ac174 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1445,6 +1445,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
   let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in
   let sort = Tacticals.New.elimination_sort_of_goal gl in
+  let mind = on_snd (fun u -> EInstance.kind (Sigma.to_evar_map sigma) u) mind in
   let Sigma (elim, sigma, p) =
     if occur_term (Sigma.to_evar_map sigma) c concl then
       build_case_analysis_scheme env sigma mind true sort
@@ -1647,6 +1648,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	let elim =
 	  try DefinedRecord (Recordops.lookup_projections ind)
 	  with Not_found ->
+            let u = EInstance.kind sigma u in
             let sigma = Sigma.Unsafe.of_evar_map sigma in
 	    let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in
 	    let elim = EConstr.of_constr elim in
@@ -2214,9 +2216,9 @@ let constructor_tac with_evars expctdnumopt i lbind =
       Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
       check_number_of_constructors expctdnumopt i nconstr;
 
-      let Sigma (cons, sigma, p) = Sigma.fresh_constructor_instance
+      let Sigma ((cons, u), sigma, p) = Sigma.fresh_constructor_instance
 	(Proofview.Goal.env gl) sigma (fst mind, i) in
-      let cons = mkConstructU cons in
+      let cons = mkConstructU (cons, EInstance.make u) in
 	
       let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
       let tac =
@@ -4033,24 +4035,25 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
 
 let guess_elim isrec dep s hyp0 gl =
   let tmptyp0 =	Tacmach.New.pf_get_hyp_typ hyp0 gl in
-  let mind,_ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
+  let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
   let evd, elimc =
-    if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl
+    if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl
     else
       let env = Tacmach.New.pf_env gl in
       let sigma = Sigma.Unsafe.of_evar_map (Tacmach.New.project gl) in
+      let u = EInstance.kind (Tacmach.New.project gl) u in
       if use_dependent_propositions_elimination () && dep
       then
-        let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma mind true s in
+        let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma (mind, u) true s in
         let ind = EConstr.of_constr ind in
         (Sigma.to_evar_map sigma, ind)
       else
-        let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in
+        let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma (mind, u) s in
         let ind = EConstr.of_constr ind in
         (Sigma.to_evar_map sigma, ind)
   in
   let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
-    evd, ((elimc, NoBindings), elimt), mkIndU mind
+    evd, ((elimc, NoBindings), elimt), mkIndU (mind, u)
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let sigma = Tacmach.New.project gl in
@@ -4637,9 +4640,10 @@ let case_type t =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let env = Tacmach.New.pf_env gl in
-  let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in
+  let ((ind, u), t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in
+  let u = EInstance.kind (Sigma.to_evar_map sigma) u in
   let s = Tacticals.New.elimination_sort_of_goal gl in
-  let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma ind s in
+  let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma (ind, u) s in
   let elimc = EConstr.of_constr elimc in
   Sigma (elim_scheme_type elimc t, evd, p)
   end }
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 10ac7135b..b9c4c6cc5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -179,9 +179,10 @@ let build_beq_scheme mode kn =
     *)
     let compute_A_equality rel_list nlist eqA ndx t =
       let lifti = ndx in
+      let sigma = Evd.empty (** FIXME *) in
       let rec aux c =
 	let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
-	match EConstr.kind Evd.empty (** FIXME *) c with
+	match EConstr.kind sigma c with
         | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
         | Var x ->
           let eid = id_of_string ("eq_"^(string_of_id x)) in
@@ -215,9 +216,10 @@ let build_beq_scheme mode kn =
         | Prod _ -> raise InductiveWithProduct
         | Lambda _-> raise (EqUnknown "abstraction")
         | LetIn _ -> raise (EqUnknown "let-in")
-        | Const kn ->
-	    (match Environ.constant_opt_value_in env kn with
-	      | None -> raise (ParameterWithoutEquality (ConstRef (fst kn)))
+        | Const (kn, u) ->
+            let u = EConstr.EInstance.kind sigma u in
+	    (match Environ.constant_opt_value_in env (kn, u) with
+	      | None -> raise (ParameterWithoutEquality (ConstRef kn))
 	      | Some c -> aux (EConstr.applist (EConstr.of_constr c,a)))
         | Proj _ -> raise (EqUnknown "projection")
         | Construct _ -> raise (EqUnknown "constructor")
@@ -373,7 +375,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
     let u,v = destruct_ind sigma type_of_pq
     in let lb_type_of_p =
         try
-          let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in
+          let c, eff = find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) in
           Proofview.tclUNIT (mkConst c, eff)
         with Not_found ->
           (* spiwack: the format of this error message should probably
@@ -445,7 +447,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
              else (
                let bl_t1, eff =
                try 
-                 let c, eff = find_scheme bl_scheme_key (out_punivs u) (*FIXME*) in
+                 let c, eff = find_scheme bl_scheme_key (fst u) (*FIXME*) in
                  mkConst c, eff
                with Not_found ->
 		 (* spiwack: the format of this error message should probably
@@ -485,13 +487,13 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   begin try Proofview.tclUNIT (destApp sigma rgt)
     with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
   end >>= fun (ind2,ca2) ->
-  begin try Proofview.tclUNIT (out_punivs (destInd sigma ind1))
+  begin try Proofview.tclUNIT (fst (destInd sigma ind1))
     with DestKO ->
       begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind1)))
         with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp1,i1) ->
-  begin try Proofview.tclUNIT (out_punivs (destInd sigma ind2))
+  begin try Proofview.tclUNIT (fst (destInd sigma ind2))
     with DestKO ->
       begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind2)))
         with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
@@ -664,7 +666,7 @@ let make_bl_scheme mode mind =
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
-    (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
+    (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 415b98f2d..c3300a361 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -166,8 +166,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
     let ctx'' = ctx' @ ctx in
-    let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
-    let cl, u = Typeclasses.typeclass_univ_instance k in
+    let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
+    let u = EConstr.EInstance.kind !evars u in
+    let cl, u = Typeclasses.typeclass_univ_instance (k, u) in
     let _, args = 
       List.fold_right (fun decl (args, args') ->
 	match decl with