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.

16 files changed, 97 insertions, 70 deletions

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) ->