Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers

50 files changed, 305 insertions, 313 deletions

diff --git a/API/API.mli b/API/API.mli
index 9f7a6ded81..e8418552c4 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -84,6 +84,11 @@ sig
     val empty : t
   end
 
+  module AUContext :
+  sig
+    type t = Univ.AUContext.t
+  end
+
   type universe_context = UContext.t
   [@@ocaml.deprecated "alias of API.Univ.UContext.t"]
 
@@ -2679,10 +2684,8 @@ sig
   val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set
   val new_Type : Names.DirPath.t -> Term.types
   val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set
-  val unsafe_type_of_global : Globnames.global_reference -> Term.types
   val constr_of_global : Prelude.global_reference -> Term.constr
   val new_univ_level : Names.DirPath.t -> Univ.Level.t
-  val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context
   val new_sort_in_family : Sorts.family -> Sorts.t
   val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds
   val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
@@ -2708,11 +2711,12 @@ sig
   val env_of_context : Environ.named_context_val -> Environ.env
   val is_polymorphic : Globnames.global_reference -> bool
 
-  val type_of_global_unsafe : Globnames.global_reference -> Term.types
+  val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
+  val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
 
   val current_dirpath : unit -> Names.DirPath.t
-  val body_of_constant_body : Declarations.constant_body -> Term.constr option
-  val body_of_constant : Names.Constant.t -> Term.constr option
+  val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option
+  val body_of_constant : Names.Constant.t -> (Term.constr * Univ.AUContext.t) option
   val add_constraints : Univ.Constraint.t -> unit
 end
 
@@ -2884,7 +2888,7 @@ sig
                   | Default_cs
   type obj_typ = Recordops.obj_typ = {
         o_DEF : Term.constr;
-        o_CTX : Univ.ContextSet.t;
+        o_CTX : Univ.AUContext.t;
         o_INJ : int option;      (** position of trivial argument *)
         o_TABS : Term.constr list;    (** ordered *)
         o_TPARAMS : Term.constr list; (** ordered *)
@@ -3043,6 +3047,7 @@ end
 module Typeclasses :
 sig
   type typeclass = Typeclasses.typeclass = {
+    cl_univs : Univ.AUContext.t;
     cl_impl : Globnames.global_reference;
     cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t;
     cl_props : Context.Rel.t;
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 159be9a582..c3c86ac5c5 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,24 @@
 =========================================
+= CHANGES BETWEEN COQ V8.7 AND COQ V8.8 =
+=========================================
+
+* ML API *
+
+We removed the following functions:
+
+- Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context
+  instead. The returned term contains De Bruijn universe variables. If you don't
+  depend on universes being instantiated, simply drop the context.
+- Universes.unsafe_type_of_global: same as above with
+  Global.type_of_global_in_context
+
+We changed the type of the following functions:
+
+- Global.body_of_constant_body: now also returns the abstract universe context.
+  The returned term contains De Bruijn universe variables.
+- Global.body_of_constant: same as above.
+
+=========================================
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
 
diff --git a/engine/termops.ml b/engine/termops.ml
index fc3291df15..1aba2bbdd1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -906,7 +906,7 @@ let collect_vars sigma c =
   aux Id.Set.empty c
 
 let vars_of_global_reference env gr =
-  let c, _ = Universes.unsafe_constr_of_global gr in
+  let c, _ = Global.constr_of_global_in_context env gr in
   vars_of_global (Global.env ()) c
 
 (* Tests whether [m] is a subterm of [t]:
diff --git a/engine/universes.ml b/engine/universes.ml
index fc441fd0b4..21854b3faa 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -319,9 +319,6 @@ let fresh_instance_from ctx inst =
   let constraints = AUContext.instantiate inst ctx in
     inst, (ctx', constraints)
 
-let unsafe_instance_from ctx =
-  (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx)
-    
 (** Fresh universe polymorphic construction *)
 
 let fresh_constant_instance env c inst =
@@ -358,34 +355,6 @@ let fresh_constructor_instance env (ind,i) inst =
     let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
     (((ind,i),inst), ctx)
 
-let unsafe_constant_instance env c =
-  let cb = lookup_constant c env in
-  match cb.Declarations.const_universes with
-  | Declarations.Monomorphic_const _ ->
-    ((c,Instance.empty), UContext.empty)
-  | Declarations.Polymorphic_const auctx ->
-    let inst, ctx = unsafe_instance_from auctx in ((c, inst), ctx)
-
-let unsafe_inductive_instance env ind = 
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> ((ind,Instance.empty), UContext.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = unsafe_instance_from auctx in ((ind,inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
-    ((ind,inst), ctx)
-
-let unsafe_constructor_instance env (ind,i) = 
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> (((ind, i),Instance.empty), UContext.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = unsafe_instance_from auctx in (((ind, i),inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
-    (((ind, i),inst), ctx)
-
 open Globnames
 
 let fresh_global_instance ?names env gr =
@@ -410,19 +379,6 @@ let fresh_inductive_instance env sp =
 let fresh_constructor_instance env sp = 
   fresh_constructor_instance env sp None
 
-let unsafe_global_instance env gr =
-  match gr with
-  | VarRef id -> mkVar id, UContext.empty
-  | ConstRef sp -> 
-     let c, ctx = unsafe_constant_instance env sp in
-       mkConstU c, ctx
-  | ConstructRef sp ->
-     let c, ctx = unsafe_constructor_instance env sp in
-       mkConstructU c, ctx
-  | IndRef sp -> 
-     let c, ctx = unsafe_inductive_instance env sp in
-       mkIndU c, ctx
-
 let constr_of_global gr =
   let c, ctx = fresh_global_instance (Global.env ()) gr in
     if not (Univ.ContextSet.is_empty ctx) then
@@ -437,9 +393,6 @@ let constr_of_global gr =
 
 let constr_of_reference = constr_of_global
 
-let unsafe_constr_of_global gr =
-  unsafe_global_instance (Global.env ()) gr
-
 let constr_of_global_univ (gr,u) =
   match gr with
   | VarRef id -> mkVar id
@@ -513,25 +466,6 @@ let type_of_reference env r =
 
 let type_of_global t = type_of_reference (Global.env ()) t
 
-let unsafe_type_of_reference env r =
-  match r with
-  | VarRef id -> Environ.named_type id env
-  | ConstRef c ->
-     let cb = Environ.lookup_constant c env in
-       Typeops.type_of_constant_type env cb.const_type
-
-  | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let (_, inst), _ = unsafe_inductive_instance env ind in
-       Inductive.type_of_inductive env (specif, inst)
-
-  | ConstructRef (ind, _ as cstr) ->
-     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-     let (_, inst), _ = unsafe_inductive_instance env ind in
-       Inductive.type_of_constructor (cstr,inst) specif
-
-let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t
-
 let fresh_sort_in_family env = function
   | InProp -> prop_sort, ContextSet.empty
   | InSet -> set_sort, ContextSet.empty
diff --git a/engine/universes.mli b/engine/universes.mli
index 5f4d212b69..8d0f106def 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -189,22 +189,11 @@ val constr_of_global : Globnames.global_reference -> constr
 (** ** DEPRECATED ** synonym of [constr_of_global] *)
 val constr_of_reference : Globnames.global_reference -> constr
 
-(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic
-    references by taking the original universe instance that is not recorded 
-    anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
-val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context
-
 (** Returns the type of the global reference, by creating a fresh instance of polymorphic 
     references and computing their instantiated universe context. (side-effect on the
     universe counter, use with care). *)
 val type_of_global : Globnames.global_reference -> types in_universe_context_set
 
-(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic
-    references by taking the original universe instance that is not recorded 
-    anywhere. The constraints are forgotten as well. 
-    USE with care. *)
-val unsafe_type_of_global : Globnames.global_reference -> types
-
 (** Full universes substitutions into terms *)
 
 val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 
diff --git a/interp/notation.ml b/interp/notation.ml
index 4067a6b945..c07a009438 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -718,13 +718,13 @@ let rebuild_arguments_scope (req,r,n,l,_) =
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
-        let scs,cls = compute_arguments_scope_full (fst(Universes.type_of_global r)(*FIXME?*)) in
+        let scs,cls = compute_arguments_scope_full (fst(Global.type_of_global_in_context (Global.env ()) r)(*FIXME?*)) in
 	(req,r,List.length scs,scs,cls)
     | ArgsScopeManual ->
 	(* Add to the manually given scopes the one found automatically
            for the extra parameters of the section. Discard the classes
            of the manually given scopes to avoid further re-computations. *)
-        let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in
+        let l',cls = compute_arguments_scope_full (fst (Global.type_of_global_in_context (Global.env ()) r)) in
 	let l1 = List.firstn n l' in
         let cls1 = List.firstn n cls in
 	(req,r,0,l1@l,cls1)
@@ -768,7 +768,7 @@ let find_arguments_scope r =
   with Not_found -> []
 
 let declare_ref_arguments_scope ref =
-  let t = Global.type_of_global_unsafe ref in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
   let (scs,cls as o) = compute_arguments_scope_full t in
   declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6614d60276..02b02db893 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1292,14 +1292,6 @@ let subst_univs_constraints subst csts =
     (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty 
 
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context (ctx, csts) = 
-  (ctx, subst_instance_constraints ctx csts)
-
-(** Substitute instance inst for ctx in universe constraints and subtyping constraints *)
-let instantiate_cumulativity_info (univcst, subtpcst) = 
-  (instantiate_univ_context univcst, instantiate_univ_context subtpcst)
-
 let make_instance_subst i = 
   let arr = Instance.to_array i in
     Array.fold_left_i (fun i acc l ->
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 53297ac462..99092a543e 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -461,12 +461,6 @@ val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abs
 
 val make_abstract_instance : abstract_universe_context -> universe_instance
 
-(** Don't use. *)
-val instantiate_univ_context : abstract_universe_context -> universe_context
-
-(** Don't use. *)
-val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
-
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.std_ppcmds
diff --git a/library/declare.ml b/library/declare.ml
index 28f108a151..154793a32d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -333,9 +333,9 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mind = Global.mind_of_delta_kn kn in
   let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
-  let sechyps,usubst,uctx = section_segment_of_mutual_inductive mind in
+  let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in
   Some (discharged_hyps kn sechyps,
-        Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie)
+        Discharge.process_inductive info repl mie)
 
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
diff --git a/library/global.ml b/library/global.ml
index e90151bffe..5b17855dce 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -126,9 +126,8 @@ let opaque_tables () = Environ.opaque_tables (env ())
 let instantiate cb c =
   let open Declarations in
   match cb.const_universes with
-  | Monomorphic_const _ -> c
-  | Polymorphic_const ctx ->
-     Vars.subst_instance_constr (Univ.AUContext.instance ctx) c
+  | Monomorphic_const _ -> c, Univ.AUContext.empty
+  | Polymorphic_const ctx -> c, ctx
 
 let body_of_constant_body cb =
   let open Declarations in
@@ -174,46 +173,45 @@ open Globnames
 (** Build a fresh instance for a given context, its associated substitution and 
     the instantiated constraints. *)
 
-let type_of_global_unsafe r = 
-  let env = env() in
+let constr_of_global_in_context env r =
+  let open Constr in
   match r with
-  | VarRef id -> Environ.named_type id env
-  | ConstRef c -> 
-    let cb = Environ.lookup_constant c env in 
-    let inst = Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) in
-    let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
-    Vars.subst_instance_constr inst ty
+  | VarRef id -> mkVar id, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = Environ.lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    mkConstU (c, Univ.make_abstract_instance univs), univs
   | IndRef ind ->
     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
-    Inductive.type_of_inductive env (specif, inst)
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkIndU (ind, Univ.make_abstract_instance univs), univs
   | ConstructRef cstr ->
-    let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
-    Inductive.type_of_constructor (cstr,inst) specif
+    let (mib,oib as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
 
 let type_of_global_in_context env r = 
   match r with
-  | VarRef id -> Environ.named_type id env, Univ.UContext.empty
+  | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
   | ConstRef c -> 
     let cb = Environ.lookup_constant c env in 
     let univs = Declareops.constant_polymorphic_context cb in
-    let inst = Univ.AUContext.instance univs in
-    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
     Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | IndRef ind ->
     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
     let univs = Declareops.inductive_polymorphic_context mib in
-    let inst = Univ.AUContext.instance univs in
-    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    let inst = Univ.make_abstract_instance univs in
+    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
     Inductive.type_of_inductive env (specif, inst), univs
   | ConstructRef cstr ->
     let (mib,oib as specif) =
       Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
     in
     let univs = Declareops.inductive_polymorphic_context mib in
-    let inst = Univ.AUContext.instance univs in
-    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
+    let inst = Univ.make_abstract_instance univs in
     Inductive.type_of_constructor (cstr,inst) specif, univs
 
 let universes_of_global env r = 
diff --git a/library/global.mli b/library/global.mli
index 5ddf54b4af..48bcfa989f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -89,8 +89,15 @@ val constant_of_delta_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
 
 val opaque_tables : unit -> Opaqueproof.opaquetab
-val body_of_constant : constant -> Term.constr option
-val body_of_constant_body : Declarations.constant_body -> Term.constr option
+
+val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option
+(** Returns the body of the constant if it has any, and the polymorphic context
+    it lives in. For monomorphic constant, the latter is empty, and for
+    polymorphic constants, the term contains De Bruijn universe variables that
+    need to be instantiated. *)
+
+val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option
+(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
 (** Global universe name <-> level mapping *)
 type universe_names = 
@@ -122,23 +129,19 @@ val is_polymorphic : Globnames.global_reference -> bool
 val is_template_polymorphic : Globnames.global_reference -> bool
 val is_type_in_type : Globnames.global_reference -> bool
 
-val type_of_global_in_context : Environ.env -> 
-  Globnames.global_reference -> Constr.types Univ.in_universe_context
-(** Returns the type of the constant in its global or local universe
+val constr_of_global_in_context : Environ.env ->
+  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+(** Returns the type of the constant in its local universe
     context. The type should not be used without pushing it's universe
     context in the environmnent of usage. For non-universe-polymorphic
     constants, it does not matter. *)
 
-val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
-(** Returns the type of the constant, forgetting its universe context if
-    it is polymorphic, use with care: for polymorphic constants, the
-    type cannot be used to produce a term used by the kernel.  For safe
-    handling of polymorphic global references, one should look at a
-    particular instantiation of the reference, in some particular
-    universe context (part of an [env] or [evar_map]), see
-    e.g. [type_of_constant_in]. If you want to create a fresh instance
-    of the reference and get its type look at [Evd.fresh_global] or
-    [Evarutil.new_global] and [Retyping.get_type_of]. *)
+val type_of_global_in_context : Environ.env -> 
+  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+(** Returns the type of the constant in its local universe
+    context. The type should not be used without pushing it's universe
+    context in the environmnent of usage. For non-universe-polymorphic
+    constants, it does not matter. *)
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
 val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context
diff --git a/library/heads.ml b/library/heads.ml
index a1cb812429..c12fa94791 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -132,7 +132,7 @@ let compute_head = function
    in
      (match body with
      | None -> RigidHead (RigidParameter cst)
-     | Some c -> kind_of_head env c)
+     | Some (c, _) -> kind_of_head env c)
 | EvalVarRef id ->
     (match Global.lookup_named id with
      | LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
diff --git a/library/impargs.ml b/library/impargs.ml
index 351addf2fa..b7125fc85d 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -431,12 +431,13 @@ let compute_mib_implicits flags manual kn =
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
         (fun i mip ->
 	  (** No need to care about constraints here *)
-	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i))))
+	  let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in
+	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
         mib.mind_packets) in
   let env_ar = push_rel_context ar env in
   let imps_one_inductive i mip =
     let ind = (kn,i) in
-    let ar = Global.type_of_global_unsafe (IndRef ind) in
+    let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
     ((IndRef ind,compute_semi_auto_implicits env flags manual ar),
      Array.mapi (fun j c ->
        (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c))
@@ -674,7 +675,7 @@ let projection_implicits env p impls =
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
-  let t = Global.type_of_global_unsafe ref in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
   let enriching = Option.default flags.auto enriching in
   let isrigid,autoimpls = compute_auto_implicits env flags enriching t in
   let l' = match l with
diff --git a/library/lib.ml b/library/lib.ml
index 439f83578d..a24d20c681 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -645,3 +645,16 @@ let discharge_con cst =
 
 let discharge_inductive (kn,i) =
   (discharge_kn kn,i)
+
+let discharge_abstract_universe_context (_, subst, abs_ctx) auctx =
+  let open Univ in
+  let len = LMap.cardinal subst in
+  let rec gen_subst i acc =
+    if i < 0 then acc
+    else
+      let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in
+      gen_subst (pred i) acc
+  in
+  let subst = gen_subst (AUContext.size auctx - 1) subst in
+  let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in
+  subst, AUContext.union abs_ctx auctx
diff --git a/library/lib.mli b/library/lib.mli
index 38a29f76e3..f1c9bfca24 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -183,3 +183,5 @@ val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
 val discharge_global : Globnames.global_reference -> Globnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
+val discharge_abstract_universe_context :
+  abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2642aeefa4..dff3548fd8 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -445,9 +445,10 @@ let error_MPfile_as_mod mp b =
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
 let argnames_of_global r =
-  let typ = Global.type_of_global_unsafe r in
+  let env = Global.env () in
+  let typ, _ = Global.type_of_global_in_context env r in
   let rels,_ =
-    decompose_prod (Reduction.whd_all (Global.env ()) typ) in
+    decompose_prod (Reduction.whd_all env typ) in
   List.rev_map fst rels
 
 let msg_of_implicit = function
@@ -878,7 +879,7 @@ let extract_constant_inline inline r ids s =
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
-	let typ = Global.type_of_global_unsafe (ConstRef kn) in
+	let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
 	let typ = Reduction.whd_all env typ in
 	if Reduction.is_arity env typ
 	  then begin
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ba46f78aa8..dc43ea7c46 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -957,7 +957,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
   let f_def = Global.lookup_constant (fst (destConst evd f)) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
-  let f_body = Option.get (Global.body_of_constant_body f_def) in
+  let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in
   let f_body = EConstr.of_constr f_body in
   let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
   let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1091,7 +1091,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     in
     let get_body const =
       match Global.body_of_constant const with
-	| Some body ->
+	| Some (body, _) ->
 	     Tacred.cbv_norm_flags
 	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	       (Global.env ())
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8ffd15f9fb..d726c1a2bb 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -407,7 +407,7 @@ let get_funs_constant mp dp =
   function const ->
     let find_constant_body const =
       match Global.body_of_constant const with
-	| Some body ->
+	| Some (body, _) ->
 	    let body = Tacred.cbv_norm_flags
 	      (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	      (Global.env ())
@@ -651,7 +651,7 @@ let build_case_scheme fa =
 (*   in  *)
   let funs =
     let (_,f,_) = fa in
-    try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+    try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
     with Not_found ->
       user_err ~hdr:"FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_reference f) in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2c5dae1cde..ff7667e991 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -851,7 +851,7 @@ let make_graph (f_ref:global_reference) =
   in
   (match Global.body_of_constant_body c_body with
      | None -> error "Cannot build a graph over an axiom!"
-     | Some body ->
+     | Some (body, _) ->
 	 let env = Global.env () in
 	 let sigma = Evd.from_env env in
 	 let extern_body,extern_type =
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6fe6888f3d..61fbca23f2 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -342,7 +342,7 @@ let pr_info f_info =
   str "function_constant_type := " ++
   (try
      Printer.pr_lconstr
-       (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
+       (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1705cac789..bc550c8b9c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -90,7 +90,7 @@ let type_of_const sigma t =
     |_ -> assert false
 
 let constr_of_global x = 
-  fst (Universes.unsafe_constr_of_global x)
+  fst (Global.constr_of_global_in_context (Global.env ()) x)
 
 let constant sl s = constr_of_global (find_reference sl s)
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 4c8827bf84..cb6a2cd695 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -337,7 +337,8 @@ let coerce_search_pattern_to_sort hpat =
     Pattern.PApp (fp, args') in
   let hr, na = splay_search_pattern 0 hpat in
   let dc, ht =
-    Reductionops.splay_prod env sigma (EConstr.of_constr (Universes.unsafe_type_of_global hr)) in
+    let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in
+    Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
   let np = List.length dc in
   if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
   let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 948aa26cac..078990a8c1 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -403,7 +403,7 @@ type coercion = {
 (* Computation of the class arity *)
 
 let reference_arity_length ref =
-  let t = Universes.unsafe_type_of_global ref in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
   List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
 
 let projection_arity_length p =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 87f29ba492..cb76df4e8a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -205,7 +205,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       else match (Stack.strip_n_app (l_us-1) sk2_effective) with
       | None -> raise Not_found
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
-  let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+  let u, ctx' = Universes.fresh_instance_from ctx None in
+  let subst = Univ.make_inverse_instance_subst u in
   let c = EConstr.of_constr c in
   let c' = subst_univs_level_constr subst c in
   let t' = EConstr.of_constr t' in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e166e0e9df..bfc6bf5cff 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -511,8 +511,8 @@ let pretype_global ?loc rigid env evd gr us =
     match us with
     | None -> evd, None
     | Some l -> 
-       let _, ctx = Universes.unsafe_constr_of_global gr in
-       let len = Univ.UContext.size ctx in
+       let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in
+       let len = Univ.AUContext.size ctx in
        interp_instance ?loc evd ~len l
   in
   let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c498089ca8..a23579609a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -134,7 +134,7 @@ let find_projection = function
 
 type obj_typ = {
   o_DEF : constr;
-  o_CTX : Univ.ContextSet.t;
+  o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (* position of trivial argument if any *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
@@ -203,10 +203,8 @@ let warn_projection_no_head_constant =
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
   let ctx = Environ.constant_context env con in
-  let u = Univ.AUContext.instance ctx in
-  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
+  let u = Univ.make_abstract_instance ctx in
   let v = (mkConstU (con,u)) in
-  let ctx = Univ.ContextSet.of_context ctx in
   let c = Environ.constant_value_in env (con,u) in
   let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
   let t = EConstr.Unsafe.to_constr t in
@@ -302,7 +300,7 @@ let error_not_structure ref =
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
   let env = Global.env () in
-  let u = Univ.AUContext.instance (Environ.constant_context env sp) in
+  let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 27d1650af0..de09edcdcb 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -57,7 +57,7 @@ type cs_pattern =
 
 type obj_typ = {
   o_DEF : constr;
-  o_CTX : Univ.ContextSet.t;
+  o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (** position of trivial argument *)
   o_TABS : constr list;    (** ordered *)
   o_TPARAMS : constr list; (** ordered *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bae831b637..d4fa266c02 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -57,6 +57,9 @@ type direction = Forward | Backward
 
 (* This module defines type-classes *)
 type typeclass = {
+  (* Universe quantification *)
+  cl_univs : Univ.AUContext.t;
+
   (* The class implementation *)
   cl_impl : global_reference;
 
@@ -111,23 +114,11 @@ let new_instance cl info glob poly impl =
 let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
 let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
 
-let typeclass_univ_instance (cl,u') =
-  let subst = 
-    let u = 
-      match cl.cl_impl with
-      | ConstRef c -> 
-        let cb = Global.lookup_constant c in
-        Univ.AUContext.instance (Declareops.constant_polymorphic_context cb)
-      | IndRef c ->
-         let mib,oib = Global.lookup_inductive c in
-         Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
-      | _ -> Univ.Instance.empty
-    in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
-      Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
-  in
-  let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in
-    { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
-      cl_props = subst_ctx cl.cl_props}, u'
+let typeclass_univ_instance (cl, u) =
+  assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
+  let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in
+    { cl with cl_context = on_snd subst_ctx cl.cl_context;
+      cl_props = subst_ctx cl.cl_props}
 
 let class_info c =
   try Refmap.find c !classes
@@ -185,7 +176,8 @@ let subst_class (subst,cl) =
     do_subst_ctx ctx in
   let do_subst_projs projs = List.smartmap (fun (x, y, z) -> 
     (x, y, Option.smartmap do_subst_con z)) projs in
-  { cl_impl = do_subst_gr cl.cl_impl;
+  { cl_univs = cl.cl_univs;
+    cl_impl = do_subst_gr cl.cl_impl;
     cl_context = do_subst_context cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
     cl_projs = do_subst_projs cl.cl_projs;
@@ -199,15 +191,14 @@ let discharge_class (_,cl) =
         let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
 	(decl' :: ctx', NamedDecl.get_id decl :: subst)
     ) ctx ([], []) in
-  let discharge_rel_context subst n rel =
+  let discharge_rel_context (subst, usubst) n rel =
     let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
-    let ctx, _ =
-      List.fold_right
-	(fun decl (ctx, k) ->
-	   RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k
-	)
-	rel ([], n)
-    in ctx
+    let fold decl (ctx, k) =
+      let map c = subst_univs_level_constr usubst (substn_vars k subst c) in
+      RelDecl.map_constr map decl :: ctx, succ k
+    in
+    let ctx, _ = List.fold_right fold rel ([], n) in
+    ctx
   in
   let abs_context cl =
     match cl.cl_impl with
@@ -227,12 +218,14 @@ let discharge_class (_,cl) =
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
-    let ctx, usubst, uctx = abs_context cl in
+    let ctx, _, _ as info = abs_context cl in
     let ctx, subst = rel_of_variable_context ctx in
-    let context = discharge_context ctx subst cl.cl_context in
-    let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
+    let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
+    let context = discharge_context ctx (subst, usubst) cl.cl_context in
+    let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
     let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in
-      { cl_impl = cl_impl';
+      { cl_univs = cl_univs';
+        cl_impl = cl_impl';
 	cl_context = context;
 	cl_props = props;
 	cl_projs = List.smartmap discharge_proj cl.cl_projs;
@@ -279,8 +272,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
         Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
   let ty, ctx = Global.type_of_global_in_context env glob in
+  let inst, ctx = Universes.fresh_instance_from ctx None in
+  let ty = Vars.subst_instance_constr inst ty in
   let ty = EConstr.of_constr ty in
-  let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in
+  let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
   let rec aux pri c ty path =
       match class_of_constr sigma ty with
       | None -> []
@@ -317,7 +312,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
 	    hints @ (path', info, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
-  let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
+  let term = Universes.constr_of_global_univ (glob, inst) in
     (*FIXME subclasses should now get substituted for each particular instance of
       the polymorphic superclass *)
     aux pri term ty [glob]
@@ -405,7 +400,7 @@ let remove_instance i =
   remove_instance_hint i.is_impl
 
 let declare_instance info local glob =
-  let ty = Global.type_of_global_unsafe glob in
+  let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a8e90ca17d..99cdbd3a36 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -16,6 +16,10 @@ type direction = Forward | Backward
 
 (** This module defines type-classes *)
 type typeclass = {
+  (** The toplevel universe quantification in which the typeclass lives. In
+      particular, [cl_props] and [cl_context] are quantified over it. *)
+  cl_univs : Univ.AUContext.t;
+
   (** The class implementation: a record parameterized by the context with defs in it or a definition if
      the class is a singleton. This acts as the class' global identifier. *)
   cl_impl : global_reference;
@@ -64,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c
 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
+val typeclass_univ_instance : typeclass puniverses -> typeclass
 
 (** Just return None if not a class *)
 val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ff12737f66..827c0e4583 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -70,7 +70,8 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
 let print_basename sp = pr_global (ConstRef sp)
 
 let print_ref reduce ref =
-  let typ = Global.type_of_global_unsafe ref in
+  let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in
+  let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in
   let typ = EConstr.of_constr typ in
   let typ =
     if reduce then
@@ -137,7 +138,7 @@ let print_renames_list prefix l =
     hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
 
 let need_expansion impl ref =
-  let typ = Global.type_of_global_unsafe ref in
+  let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in
   let ctx = prod_assum typ in
   let nprods = List.count is_local_assum ctx in
   not (List.is_empty impl) && List.length impl >= nprods &&
@@ -532,7 +533,9 @@ let print_constant with_values sep sp =
       begin
         match cb.const_universes with
         | Monomorphic_const ctx -> ctx
-        | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+        | Polymorphic_const ctx ->
+          let inst = Univ.AUContext.instance ctx in
+          Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
       end
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
@@ -542,7 +545,8 @@ let print_constant with_values sep sp =
         Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
       | Polymorphic_const ctx ->
         assert(Univ.ContextSet.is_empty body_uctxs);
-        Univ.instantiate_univ_context ctx
+        let inst = Univ.AUContext.instance ctx in
+        Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
   in
   let ctx =
     Evd.evar_universe_context_of_binders
@@ -557,9 +561,10 @@ let print_constant with_values sep sp =
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
 	Printer.pr_universe_ctx sigma univs
-    | _ ->
+    | Some (c, ctx) ->
+        let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
-	(if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++
+	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
         Printer.pr_universe_ctx sigma univs)
 
 let gallina_print_constant_with_infos sp =
@@ -797,9 +802,11 @@ let print_opaque_name qid =
     | IndRef (sp,_) ->
         print_inductive sp
     | ConstructRef cstr as gr ->
-        let open EConstr in
-	let ty = Universes.unsafe_type_of_global gr in
+	let ty, ctx = Global.type_of_global_in_context env gr in
+	let inst = Univ.AUContext.instance ctx in
+	let ty = Vars.subst_instance_constr inst ty in
 	let ty = EConstr.of_constr ty in
+        let open EConstr in
 	print_typed_value (mkConstruct cstr, ty)
     | VarRef id ->
         env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2e0e6d2845..5c7dcdc10f 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -110,6 +110,17 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
   brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
 
+let instantiate_cumulativity_info cumi =
+  let open Univ in
+  let univs = ACumulativityInfo.univ_context cumi in
+  let subtyp = ACumulativityInfo.subtyp_context cumi in
+  let expose ctx =
+    let inst = AUContext.instance ctx in
+    let cst = AUContext.instantiate inst ctx in
+    UContext.make (inst, cst)
+  in
+  CumulativityInfo.make (expose univs, expose subtyp)
+
 let print_mutual_inductive env mind mib =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
   in
@@ -133,7 +144,7 @@ let print_mutual_inductive env mind mib =
          | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
          | Cumulative_ind cumi ->
            Printer.pr_cumulativity_info
-             sigma (Univ.instantiate_cumulativity_info cumi))
+             sigma (instantiate_cumulativity_info cumi))
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -191,7 +202,7 @@ let print_record env mind mib =
     | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
     | Cumulative_ind cumi ->
       Printer.pr_cumulativity_info
-        sigma (Univ.instantiate_cumulativity_info cumi)
+        sigma (instantiate_cumulativity_info cumi)
   )
 
 let pr_mutual_inductive_body env mind mib =
diff --git a/stm/stm.ml b/stm/stm.ml
index fd3d418c10..7c96208546 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1576,8 +1576,10 @@ end = struct (* {{{ *)
         let uc =
           Option.get
             (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+        (** We only manipulate monomorphic terms here. *)
+        let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
         let pr =
-          Future.from_val (Option.get (Global.body_of_constant_body c)) in
+          Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
         let uc =
           Future.chain
             ~pure:true uc Univ.hcons_universe_context_set in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index e058806a35..2d2a0c1b2a 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -46,28 +46,15 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
     let sigma, nf = Evarutil.nf_evars_and_universes sigma in
       (nf c', Evd.evar_universe_context sigma), eff
   else
-    let mib,mip = Inductive.lookup_mind_specif env ind in
-    let ctx = Declareops.inductive_polymorphic_context mib in
-    let u = Univ.AUContext.instance ctx in
-    let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
-    let ctxset = Univ.ContextSet.of_context ctx in
-    let ectx = Evd.evar_universe_context_of ctxset in
-    let sigma = Evd.merge_universe_context sigma ectx in
-    let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
+    let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+    let sigma, c = build_induction_scheme env sigma pind dep sort in
       (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let ctx = 
-    let mib,mip = Inductive.lookup_mind_specif env ind in
-      Declareops.inductive_polymorphic_context mib
-  in
-  let u = Univ.AUContext.instance ctx in
-  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
-  let ctxset = Univ.ContextSet.of_context ctx in
-  let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in
-  let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in
+  let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+  let sigma, c = build_induction_scheme env sigma pind dep sort in
     c, Evd.evar_universe_context sigma
  
 let rect_scheme_kind_from_type =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c2c80e6305..a572508d47 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -937,7 +937,7 @@ let make_extern pri pat tacast =
 
 let make_mode ref m = 
   let open Term in
-  let ty = Global.type_of_global_unsafe ref in
+  let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in
   let ctx, t = decompose_prod ty in
   let n = List.length ctx in
   let m' = Array.of_list m in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2e3a4e33b3..c979b8b040 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5003,9 +5003,19 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
     Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl
   in
   let cst = Impargs.with_implicit_protection cst () in
-  (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
-  let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
-  let lem = EConstr.of_constr lem in
+  let lem =
+    if const.Entries.const_entry_polymorphic then
+      let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in
+      (** Hack: the kernel may generate definitions whose universe variables are
+          not the same as requested in the entry because of constraints delayed
+          in the body, even in polymorphic mode. We mimick what it does for now
+          in hope it is fixed at some point. *)
+      let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in
+      let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in
+      let u = Univ.UContext.instance uctx in
+      mkConstU (cst, EInstance.make u)
+    else mkConst cst
+  in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in
   let eff = private_con_of_con (Global.safe_env ()) cst in
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v
index cd9cad4064..7bed956f3e 100644
--- a/test-suite/bugs/closed/HoTT_coq_123.v
+++ b/test-suite/bugs/closed/HoTT_coq_123.v
@@ -104,11 +104,15 @@ Record Functor (C D : PreCategory) :=
     morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d)
   }.
 
+(** Workaround to simpl losing universe constraints, see bug #5645. *)
+Ltac simpl' :=
+  simpl; match goal with [ |- ?P ] => let T := type of P in idtac end.
+
 Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
 : IsTrunc n (forall a, P a) | 100.
 Proof.
     generalize dependent P.
-  induction n as [ | n' IH]; (simpl; intros P ?).
+  induction n as [ | n' IH]; (simpl'; intros P ?).
   - admit.
   - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit.
 Defined.
diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v
new file mode 100644
index 0000000000..b736b734fd
--- /dev/null
+++ b/test-suite/success/abstract_poly.v
@@ -0,0 +1,20 @@
+Set Universe Polymorphism.
+
+Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x.
+Inductive unit@{i} : Type@{i} := tt.
+
+Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n.
+Proof.
+intros m n P e p.
+abstract (rewrite e in p; exact p).
+Defined.
+
+Check foo_subproof@{Set Set}.
+
+Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n.
+Proof.
+intros m n P e p.
+abstract (rewrite e in p; exact p).
+Defined.
+
+Check bar_subproof@{Set Set Set}.
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index db07bbd068..86bbf46a35 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -187,7 +187,7 @@ let rec traverse current ctx accu t = match kind_of_term t with
   let body () = id |> Global.lookup_named |> NamedDecl.get_value in
   traverse_object accu body (VarRef id)
 | Const (kn, _) ->
-  let body () = Global.body_of_constant_body (lookup_constant kn) in
+  let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
   traverse_object accu body (ConstRef kn)
 | Ind ((mind, _) as ind, _) ->
   traverse_inductive accu mind (IndRef ind)
@@ -200,7 +200,7 @@ let rec traverse current ctx accu t = match kind_of_term t with
     | Lambda(_,_,oty), Const (kn, _)
       when Vars.noccurn 1 oty &&
       not (Declareops.constant_has_body (lookup_constant kn)) ->
-        let body () = Global.body_of_constant_body (lookup_constant kn) in
+        let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in
         traverse_object
           ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
     | _ ->
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 248224e6b7..59920742d8 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -105,7 +105,7 @@ let mkFullInd (ind,u) n =
     else mkIndU (ind,u)
 
 let check_bool_is_defined () =
-  try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in ()
+  try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in ()
   with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
diff --git a/vernac/class.ml b/vernac/class.ml
index 0b510bbcf0..be682977e5 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -62,7 +62,9 @@ let explain_coercion_error g = function
 (* Verifications pour l'ajout d'une classe *)
 
 let check_reference_arity ref =
-  if not (Reductionops.is_arity (Global.env()) Evd.empty (EConstr.of_constr (Global.type_of_global_unsafe ref))) (** FIXME *) then
+  let env = Global.env () in
+  let c, _ = Global.type_of_global_in_context env ref in
+  if not (Reductionops.is_arity env Evd.empty (EConstr.of_constr c)) (** FIXME *) then
     raise (CoercionError (NotAClass ref))
 
 let check_arity = function
@@ -252,7 +254,7 @@ let warn_uniform_inheritance =
 
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
-  let t = Global.type_of_global_unsafe coef in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let tg,lp = prods_of t in
   let llp = List.length lp in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a528b96407..ab1892a18e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -68,7 +68,7 @@ let _ =
 let existing_instance glob g info =
   let c = global g in
   let info = Option.default Hints.empty_hint_info info in
-  let instance = Global.type_of_global_unsafe c in
+  let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
   let _, r = decompose_prod_assum instance in
     match class_of_constr Evd.empty (EConstr.of_constr r) with
       | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
@@ -164,7 +164,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
     let ctx'' = ctx' @ ctx 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 cl = Typeclasses.typeclass_univ_instance (k, u) in
     let _, args = 
       List.fold_right (fun decl (args, args') ->
 	match decl with
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index b6308aba00..474c0b4dd2 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -77,42 +77,36 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
     let ctx = List.rev mip.mind_arity_ctxt in
       mkArity (List.rev ctx, Type ar.template_level), true
 
-let process_inductive (sechyps,abs_ctx) modlist mib =
+let process_inductive (sechyps,_,_ as info) modlist mib =
+  let sechyps = Lib.named_of_variable_context sechyps in
   let nparams = mib.mind_nparams in
-  let subst, univs =
+  let subst, ind_univs =
     match mib.mind_universes with
-    | Monomorphic_ind ctx -> Univ.Instance.empty, ctx
+    | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
     | Polymorphic_ind auctx ->
-      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+      let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let auctx = Univ.AUContext.repr auctx in
+      subst, Polymorphic_ind_entry auctx
     | Cumulative_ind cumi ->
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
-      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+      let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
+      let auctx = Univ.AUContext.repr auctx in
+      subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
   in
+  let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
     Array.map_to_list
       (fun mip ->
 	let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
-	let arity = expmod_constr modlist ty in
-	let arity = Vars.subst_instance_constr subst arity in
-	let lc = Array.map 
-	  (fun c -> Vars.subst_instance_constr subst (expmod_constr modlist c))
-	  mip.mind_user_lc 
-	in
+        let arity = discharge ty in
+        let lc = Array.map discharge mip.mind_user_lc  in
 	  (mip.mind_typename,
 	   arity, template,
 	   Array.to_list mip.mind_consnames,
 	   Array.to_list lc))
       mib.mind_packets in
-  let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
+  let sechyps' = Context.Named.map discharge sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
-  let abs_ctx = Univ.instantiate_univ_context abs_ctx in
-  let univs = Univ.UContext.union abs_ctx univs in
-  let ind_univs =
-    match mib.mind_universes with
-    | Monomorphic_ind _ -> Monomorphic_ind_entry univs
-    | Polymorphic_ind _ -> Polymorphic_ind_entry univs
-    | Cumulative_ind _ ->
-      Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None
diff --git a/vernac/discharge.mli b/vernac/discharge.mli
index a0dabe2f46..c8c7e3b8b8 100644
--- a/vernac/discharge.mli
+++ b/vernac/discharge.mli
@@ -11,5 +11,4 @@ open Entries
 open Opaqueproof
 
 val process_inductive :
-  ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context)
-  -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+  Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 86dcb6d4dc..784c6d3387 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -909,7 +909,7 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
-      let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in
+      let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6d93f0e410..3d97a767c8 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -383,9 +383,8 @@ let do_mutual_induction_scheme lnamedepindsort =
 	 match inst with
 	 | None ->
 	    let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
-	    let ctxs = Univ.ContextSet.of_context ctx in
-	    let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in
-	    let u = Univ.UContext.instance ctx in
+	    let u, ctx = Universes.fresh_instance_from ctx None in
+	    let evd = Evd.from_ctx (Evd.evar_universe_context_of ctx) in
 	      evd, (ind,u), Some u
 	 | Some ui -> evd, (ind, ui), inst
        in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2eeaf4d5dc..645320c603 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -44,12 +44,15 @@ let call_hook fix_exn hook l c =
 
 (* Support for mutually proved theorems *)
 
-let retrieve_first_recthm = function
+let retrieve_first_recthm uctx = function
   | VarRef id ->
       (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
-      (Global.body_of_constant_body cb, is_opaque cb)
+      let (_, uctx) = UState.universe_context uctx in
+      let inst = Univ.UContext.instance uctx in
+      let map (c, ctx) = Vars.subst_instance_constr inst c in
+      (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
   | _ -> assert false
 
 let adjust_guardness_conditions const = function
@@ -412,7 +415,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
         let other_thms_data =
           if List.is_empty other_thms then [] else
             (* there are several theorems defined mutually *)
-            let body,opaq = retrieve_first_recthm ref in
+            let body,opaq = retrieve_first_recthm ctx ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
 	    let ctx = UState.context_set (*FIXME*) ctx in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5a1c260b1f..4b1565d3ce 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -285,7 +285,7 @@ type obligation =
   { obl_name : Id.t;
     obl_type : types;
     obl_location : Evar_kinds.t Loc.located;
-    obl_body : constant obligation_body option;
+    obl_body : pconstant obligation_body option;
     obl_status : bool * Evar_kinds.obligation_definition_status;
     obl_deps : Int.Set.t;
     obl_tac : unit Proofview.tactic option;
@@ -358,18 +358,8 @@ let _ =
 
 let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
-let get_body obl =
-  match obl.obl_body with
-  | None -> None
-  | Some (DefinedObl c) ->
-    let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in
-    let pc = (c, u) in
-      Some (DefinedObl pc)
-  | Some (TermObl c) ->
-      Some (TermObl c)
-
 let get_obligation_body expand obl =
-  match get_body obl with
+  match obl.obl_body with
   | None -> None
   | Some c ->
      if expand && snd obl.obl_status == Evar_kinds.Expand then
@@ -664,7 +654,7 @@ let declare_obligation prg obl body ty uctx =
 	definition_message obl.obl_name;
 	true, { obl with obl_body =
 	    if poly then
-	      Some (DefinedObl constant)
+	      Some (DefinedObl (constant, Univ.UContext.instance uctx))
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
 
@@ -892,20 +882,22 @@ let obligation_hook prg obl num auto ctx' _ gr =
        if not transparent then err_not_transp ()
     | _ -> ()
 in
-  let obl = { obl with obl_body = Some (DefinedObl cst) } in
-  let () = if transparent then add_hint true prg cst in
-  let obls = Array.copy obls in
-  let _ = obls.(num) <- obl in
   let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
-  let ctx' =
+  let inst, ctx' =
     if not (pi2 prg.prg_kind) (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
       let evd = Evd.from_env (Global.env ()) in
       let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
-        Evd.evar_universe_context ctx'
-    else ctx'
+      Univ.Instance.empty, Evd.evar_universe_context ctx'
+    else
+      let (_, uctx) = UState.universe_context ctx' in
+      Univ.UContext.instance uctx, ctx'
   in
+  let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
+  let () = if transparent then add_hint true prg cst in
+  let obls = Array.copy obls in
+  let _ = obls.(num) <- obl in
   let prg = { prg with prg_ctx = ctx' } in
   let () =
     try ignore (update_obls prg obls (pred rem))
@@ -1132,7 +1124,7 @@ let admit_prog prg =
               (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
-              obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
+              obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
         | Some _ -> ())
       obls;
     ignore(update_obls prg obls 0)
diff --git a/vernac/record.ml b/vernac/record.ml
index 366f504545..63ca227862 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,16 +265,10 @@ let warn_non_primitive_record =
 let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
-  let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let poly = Declareops.inductive_is_polymorphic mib in
-  let ctx =
-    match mib.mind_universes with
-    | Monomorphic_ind ctx -> ctx
-    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
-    | Cumulative_ind cumi -> 
-      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
-  in
+  let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in
+  let u = Univ.UContext.instance ctx in
+  let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
@@ -334,8 +328,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
-		    const_entry_universes =
-		      if poly then ctx else Univ.UContext.empty;
+		    const_entry_universes = ctx;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in
@@ -431,6 +424,12 @@ let declare_structure finite univs id idbuild paramimpls params arity template
   let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
+  let fields =
+    if poly then
+      let subst, _ = Univ.abstract_universes ctx in
+      Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields
+    else fields
+  in
   let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
   let build = ConstructRef cstr in
   let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
@@ -518,8 +517,18 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
       | None -> None)
       params, params
   in
+  let univs, ctx_context, fields =
+    if poly then
+      let usubst, auctx = Univ.abstract_universes ctx in
+      let map c = Vars.subst_univs_level_constr usubst c in
+      let fields = Context.Rel.map map fields in
+      let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
+      auctx, ctx_context, fields
+    else Univ.AUContext.empty, ctx_context, fields
+  in
   let k =
-    { cl_impl = impl;
+    { cl_univs = univs;
+      cl_impl = impl;
       cl_strict = !typeclasses_strict;
       cl_unique = !typeclasses_unique;
       cl_context = ctx_context;
@@ -530,10 +539,11 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
 
 
 let add_constant_class cst =
-  let ty = Universes.unsafe_type_of_global (ConstRef cst) in
+  let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in
   let ctx, arity = decompose_prod_assum ty in
   let tc = 
-    { cl_impl = ConstRef cst;
+    { cl_univs = univs;
+      cl_impl = ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
       cl_props = [LocalAssum (Anonymous, arity)];
       cl_projs = [];
@@ -547,12 +557,13 @@ let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
-    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in
-    let ty = Inductive.type_of_inductive
-      (push_rel_context ctx (Global.env ()))
-      ((mind,oneind),inst)
-    in
-      { cl_impl = IndRef ind;
+    let univs = Declareops.inductive_polymorphic_context mind in
+    let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in
+    let env = push_rel_context ctx env in
+    let inst = Univ.make_abstract_instance univs in
+    let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
+      { cl_univs = univs;
+        cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
 	cl_props = [LocalAssum (Anonymous, ty)];
 	cl_projs = [];
diff --git a/vernac/search.ml b/vernac/search.ml
index 788a2aa4a9..0f56f81e74 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -78,14 +78,14 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   | "CONSTANT" ->
     let cst = Global.constant_of_delta_kn kn in
     let gr = ConstRef cst in
-    let typ = Global.type_of_global_unsafe gr in
+    let (typ, _) = Global.type_of_global_in_context (Global.env ()) gr in
       fn gr env typ
   | "INDUCTIVE" ->
     let mind = Global.mind_of_delta_kn kn in
     let mib = Global.lookup_mind mind in
     let iter_packet i mip =
       let ind = (mind, i) in
-      let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
+      let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
       let i = (ind, u) in
       let typ = Inductiveops.type_of_inductive env i in
       let () = fn (IndRef ind) env typ in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bbec28afff..8a647c6c18 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -986,7 +986,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
 
   let sr = smart_global reference in
   let inf_names =
-    let ty = Global.type_of_global_unsafe sr in
+    let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in
     Impargs.compute_implicits_names (Global.env ()) ty
   in
   let prev_names =