Merge PR #8694: Various cleanups of universe apis

39 files changed, 233 insertions, 285 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8ab3ce821e..3385b78958 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -74,6 +74,12 @@ let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
 let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
 
+let mkRef (gr,u) = let open GlobRef in match gr with
+  | ConstRef c -> mkConstU (c,u)
+  | IndRef ind -> mkIndU (ind,u)
+  | ConstructRef c -> mkConstructU (c,u)
+  | VarRef x -> mkVar x
+
 let applist (f, arg) = mkApp (f, Array.of_list arg)
 
 let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
@@ -166,6 +172,13 @@ let destProj sigma c = match kind sigma c with
 | Proj (p, c) -> (p, c)
 | _ -> raise DestKO
 
+let destRef sigma c = let open GlobRef in match kind sigma c with
+  | Var x -> VarRef x, EInstance.empty
+  | Const (c,u) -> ConstRef c, u
+  | Ind (ind,u) -> IndRef ind, u
+  | Construct (c,u) -> ConstructRef c, u
+  | _ -> raise DestKO
+
 let decompose_app sigma c =
   match kind sigma c with
     | App (f,cl) -> (f, Array.to_list cl)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f897448557..1edc0ee12b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -122,6 +122,8 @@ val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> t -> t
 
+val mkRef : GlobRef.t * EInstance.t -> t
+
 val applist : t * t list -> t
 
 val mkProd_or_LetIn : rel_declaration -> t -> t
@@ -180,6 +182,8 @@ val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
 
+val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
+
 val decompose_app : Evd.evar_map -> t -> t * t list
 
 (** Pops lambda abstractions until there are no more, skipping casts. *)
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 37e83b6238..bb43808542 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -4,8 +4,8 @@ UnivSubst
 UnivProblem
 UnivMinim
 Universes
-Univops
 UState
+Univops
 Nameops
 Evar_kinds
 Evd
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 13356627f0..f9d9ce3569 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -549,7 +549,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
             if Id.Set.mem id' ids then
               raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
           in
-          Id.Set.iter check (Environ.vars_of_global env c)
+          Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c))
         in
         c
 
diff --git a/engine/evd.ml b/engine/evd.ml
index d7b03a84f1..eafdc4cb46 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -818,7 +818,7 @@ let fresh_constructor_instance ?loc env evd c =
   with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
 
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
+  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
 
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 1244074d50..ee0c3d210e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -912,9 +912,9 @@ let occur_in_global env id constr =
 
 let occur_var env sigma id c =
   let rec occur_rec c =
-    match EConstr.kind sigma c with
-    | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c)
-    | _ -> EConstr.iter sigma occur_rec c
+    match EConstr.destRef sigma c with
+    | gr, _ -> occur_in_global env id gr
+    | exception DestKO -> EConstr.iter sigma occur_rec c
   in
   try occur_rec c; false with Occur -> true
 
@@ -961,9 +961,7 @@ let collect_vars sigma c =
   | _ -> EConstr.fold sigma aux vars c in
   aux Id.Set.empty c
 
-let vars_of_global_reference env gr =
-  let c, _ = Global.constr_of_global_in_context env gr in
-  vars_of_global env c
+let vars_of_global_reference = vars_of_global
 
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
@@ -1458,12 +1456,9 @@ let clear_named_body id env =
 
 let global_vars_set env sigma constr =
   let rec filtrec acc c =
-    let acc = match EConstr.kind sigma c with
-    | Var _ | Const _ | Ind _ | Construct _ ->
-      Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
-    | _ -> acc
-    in
-    EConstr.fold sigma filtrec acc c
+    match EConstr.destRef sigma c with
+    | gr, _ -> Id.Set.union (vars_of_global env gr) acc
+    | exception DestKO -> EConstr.fold sigma filtrec acc c
   in
   filtrec Id.Set.empty constr
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 64e3977d68..f7b9469ae8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -118,7 +118,9 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
 val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
+
 val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
+[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
 
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
diff --git a/engine/uState.ml b/engine/uState.ml
index 29cb3c9bcc..aa7ec63a6f 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -406,12 +406,25 @@ let check_univ_decl ~poly uctx decl =
       (Univ.ContextSet.constraints uctx.uctx_local);
   ctx
 
+let restrict_universe_context (univs, csts) keep =
+  let open Univ in
+  let removed = LSet.diff univs keep in
+  if LSet.is_empty removed then univs, csts
+  else
+  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+  let g = UGraph.empty_universes in
+  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+  let g = UGraph.merge_constraints csts g in
+  let allkept = LSet.diff allunivs removed in
+  let csts = UGraph.constraints_for ~kept:allkept g in
+  (LSet.inter univs keep, csts)
+
 let restrict ctx vars =
   let vars = Univ.LSet.union vars ctx.uctx_seff_univs in
   let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
       (fst ctx.uctx_names) vars
   in
-  let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
+  let uctx' = restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
 let demote_seff_univs entry uctx =
diff --git a/engine/uState.mli b/engine/uState.mli
index f833508ebf..8053a7bf83 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -13,6 +13,7 @@
     primitives when needed. *)
 
 open Names
+open Univ
 
 exception UniversesDiffer
 
@@ -91,6 +92,16 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
 
 (** {5 Unification} *)
 
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+   the universes in [keep]. The constraints [csts] are adjusted so
+   that transitive constraints between remaining universes (those in
+   [keep] and those not in [univs]) are preserved. *)
+val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+
+(** [restrict uctx ctx] restricts the local universes of [uctx] to
+   [ctx] extended by local named universes and side effect universes
+   (from [demote_seff_univs]). Transitive constraints between retained
+   universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
 val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index b07d4848ff..23ab30eb75 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -11,7 +11,6 @@
 open Sorts
 open Names
 open Constr
-open Environ
 open Univ
 
 (* Generator of levels *)
@@ -32,103 +31,51 @@ let new_univ dp = Univ.Universe.make (new_univ_level dp)
 let new_Type dp = mkType (new_univ dp)
 let new_Type_sort dp = Type (new_univ dp)
 
-let fresh_universe_instance ctx =
-  let init _ = new_univ_level () in
-  Instance.of_array (Array.init (AUContext.size ctx) init)
+let fresh_instance auctx =
+  let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+  let ctx = Array.fold_right LSet.add inst LSet.empty in
+  let inst = Instance.of_array inst in
+  inst, (ctx, AUContext.instantiate inst auctx)
 
-let fresh_instance_from_context ctx =
-  let inst = fresh_universe_instance ctx in
-  let constraints = AUContext.instantiate inst ctx in
-    inst, constraints
-
-let fresh_instance ctx =
-  let ctx' = ref LSet.empty in
-  let init _ =
-    let u = new_univ_level () in
-    ctx' := LSet.add u !ctx'; u
-  in
-  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
-  in !ctx', inst
-
-let existing_instance ctx inst =
+let existing_instance ?loc auctx inst =
   let () =
     let len1 = Array.length (Instance.to_array inst)
-    and len2 = AUContext.size ctx in
+    and len2 = AUContext.size auctx in
       if not (len1 == len2) then
-        CErrors.user_err ~hdr:"Universes"
-          Pp.(str "Polymorphic constant expected " ++ int len2 ++
-              str" levels but was given " ++ int len1)
+        CErrors.user_err ?loc ~hdr:"Universes"
+          Pp.(str "Universe instance should have length " ++ int len2 ++ str ".")
       else ()
-  in LSet.empty, inst
-
-let fresh_instance_from ctx inst =
-  let ctx', inst =
-    match inst with
-    | Some inst -> existing_instance ctx inst
-    | None -> fresh_instance ctx
   in
-  let constraints = AUContext.instantiate inst ctx in
-    inst, (ctx', constraints)
+  inst, (LSet.empty, AUContext.instantiate inst auctx)
 
-(** Fresh universe polymorphic construction *)
+let fresh_instance_from ?loc ctx = function
+  | Some inst -> existing_instance ?loc ctx inst
+  | None -> fresh_instance ctx
 
-let fresh_constant_instance env c inst =
-  let cb = lookup_constant c env in
-  match cb.Declarations.const_universes with
-  | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_const auctx ->
-    let inst, ctx =
-      fresh_instance_from auctx inst
-    in
-    ((c, inst), ctx)
-
-let fresh_inductive_instance env ind inst =
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    ((ind,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind uactx ->
-    let inst, ctx = (fresh_instance_from uactx) inst in
-     ((ind,inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx =
-      fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
-    in ((ind,inst), ctx)
-
-let fresh_constructor_instance env (ind,i) inst =
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = fresh_instance_from auctx  inst in
-        (((ind,i),inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
-    (((ind,i),inst), ctx)
+(** Fresh universe polymorphic construction *)
 
 open Globnames
 
-let fresh_global_instance ?names env gr =
-  match gr with
-  | VarRef id -> mkVar id, ContextSet.empty
-  | ConstRef sp ->
-     let c, ctx = fresh_constant_instance env sp names in
-       mkConstU c, ctx
-  | ConstructRef sp ->
-     let c, ctx = fresh_constructor_instance env sp names in
-       mkConstructU c, ctx
-  | IndRef sp ->
-     let c, ctx = fresh_inductive_instance env sp names in
-       mkIndU c, ctx
+let fresh_global_instance ?loc ?names env gr =
+  let auctx = Environ.universes_of_global env gr in
+  let u, ctx = fresh_instance_from ?loc auctx names in
+  u, ctx
+
+let fresh_constant_instance env c =
+  let u, ctx = fresh_global_instance env (ConstRef c) in
+  (c, u), ctx
 
-let fresh_constant_instance env sp =
-  fresh_constant_instance env sp None
+let fresh_inductive_instance env ind =
+  let u, ctx = fresh_global_instance env (IndRef ind) in
+  (ind, u), ctx
 
-let fresh_inductive_instance env sp =
-  fresh_inductive_instance env sp None
+let fresh_constructor_instance env c =
+  let u, ctx = fresh_global_instance env (ConstructRef c) in
+  (c, u), ctx
 
-let fresh_constructor_instance env sp =
-  fresh_constructor_instance env sp None
+let fresh_global_instance ?loc ?names env gr =
+  let u, ctx = fresh_global_instance ?loc ?names env gr in
+  mkRef (gr, u), ctx
 
 let constr_of_global gr =
   let c, ctx = fresh_global_instance (Global.env ()) gr in
@@ -142,12 +89,7 @@ let constr_of_global gr =
               str " would forget universes.")
     else c
 
-let constr_of_global_univ (gr,u) =
-  match gr with
-  | VarRef id -> mkVar id
-  | ConstRef sp -> mkConstU (sp,u)
-  | ConstructRef sp -> mkConstructU (sp,u)
-  | IndRef sp -> mkIndU (sp,u)
+let constr_of_global_univ = mkRef
 
 let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, ContextSet.empty
@@ -166,52 +108,26 @@ open Declarations
 let type_of_reference env r =
   match r with
   | VarRef id -> Environ.named_type id env, ContextSet.empty
+
   | ConstRef c ->
      let cb = Environ.lookup_constant c env in
      let ty = cb.const_type in
-     begin
-       match cb.const_universes with
-       | Monomorphic_const _ -> ty, ContextSet.empty
-       | Polymorphic_const auctx ->
-         let inst, ctx = fresh_instance_from auctx None in
-         Vars.subst_instance_constr inst ty, ctx
-     end
+     let auctx = Declareops.constant_polymorphic_context cb in
+     let inst, ctx = fresh_instance auctx in
+     Vars.subst_instance_constr inst ty, ctx
+
   | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     begin
-       match mib.mind_universes with
-       | Monomorphic_ind _ ->
-         let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
-         ty, ContextSet.empty
-       | Polymorphic_ind auctx ->
-         let inst, ctx = fresh_instance_from auctx  None in
-         let ty = Inductive.type_of_inductive env (specif, inst) in
-         ty, ctx
-       | Cumulative_ind cumi ->
-         let inst, ctx =
-           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
-         in
-         let ty = Inductive.type_of_inductive env (specif, inst) in
-         ty, ctx
-     end
-
-  | ConstructRef cstr ->
-    let (mib,oib as specif) =
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
-    in
-    begin
-       match mib.mind_universes with
-       | Monomorphic_ind _ ->
-         Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
-       | Polymorphic_ind auctx ->
-         let inst, ctx = fresh_instance_from auctx None in
-         Inductive.type_of_constructor (cstr,inst) specif, ctx
-       | Cumulative_ind cumi ->
-         let inst, ctx =
-           fresh_instance_from (ACumulativityInfo.univ_context cumi) None
-         in
-         Inductive.type_of_constructor (cstr,inst) specif, ctx
-     end
+    let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
+    let auctx = Declareops.inductive_polymorphic_context mib in
+    let inst, ctx = fresh_instance auctx in
+    let ty = Inductive.type_of_inductive env (specif, inst) in
+    ty, ctx
+
+  | ConstructRef (ind,_ as cstr) ->
+    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+    let auctx = Declareops.inductive_polymorphic_context mib in
+    let inst, ctx = fresh_instance auctx in
+    Inductive.type_of_constructor (cstr,inst) specif, ctx
 
 let type_of_global t = type_of_reference (Global.env ()) t
 
@@ -225,8 +141,7 @@ let fresh_sort_in_family = function
 let new_sort_in_family sf =
   fst (fresh_sort_in_family sf)
 
-let extend_context (a, ctx) (ctx') =
-  (a, ContextSet.union ctx ctx')
+let extend_context = Univ.extend_in_context_set
 
 let new_global_univ () =
   let u = fresh_level () in
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 439424934c..c2e9d0c696 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -23,20 +23,24 @@ val set_remote_new_univ_id : universe_id RemoteCounter.installer
 
 val new_univ_id : unit -> universe_id
 val new_univ_level : unit -> Level.t
+
 val new_univ : unit -> Universe.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
 val new_Type : unit -> types
+[@@ocaml.deprecated "Use [new_univ_level]"]
 val new_Type_sort : unit -> Sorts.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
 
 val new_global_univ : unit -> Universe.t in_universe_context_set
 val new_sort_in_family : Sorts.family -> Sorts.t
+[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
 
 (** Build a fresh instance for a given context, its associated substitution and
     the instantiated constraints. *)
 
-val fresh_instance_from_context : AUContext.t ->
-  Instance.t constrained
+val fresh_instance : AUContext.t -> Instance.t in_universe_context_set
 
-val fresh_instance_from : AUContext.t -> Instance.t option ->
+val fresh_instance_from : ?loc:Loc.t -> AUContext.t -> Instance.t option ->
   Instance.t in_universe_context_set
 
 val fresh_sort_in_family : Sorts.family ->
@@ -48,7 +52,7 @@ val fresh_inductive_instance : env -> inductive ->
 val fresh_constructor_instance : env -> constructor ->
   pconstructor in_universe_context_set
 
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
   constr in_universe_context_set
 
 val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
@@ -63,9 +67,11 @@ val fresh_universe_context_set_instance : ContextSet.t ->
 val global_of_constr : constr -> GlobRef.t puniverses
 
 val constr_of_global_univ : GlobRef.t puniverses -> constr
+[@@ocaml.deprecated "Use [Constr.mkRef]"]
 
 val extend_context : 'a in_universe_context_set -> ContextSet.t ->
   'a in_universe_context_set
+[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
 
 (** Create a fresh global in the global environment, without side effects.
     BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
diff --git a/engine/univNames.ml b/engine/univNames.ml
index e89dcedb9c..a71f9c5736 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -86,7 +86,7 @@ let register_universe_binders ref ubinders =
       part of the code that depends on the internal representation of names in
       abstract contexts, but removing it requires quite a rework of the
       callers. *)
-  let univs = AUContext.instance (Global.universes_of_global ref) in
+  let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
   let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
   let map lvl =
     try LMap.find lvl revmap
diff --git a/engine/univops.ml b/engine/univops.ml
index 7f9672f828..53c42023ad 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -8,30 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Univ
-open Constr
+let universes_of_constr = Vars.universes_of_constr
 
-let universes_of_constr c =
-  let rec aux s c =
-    match kind c with
-    | Const (c, u) ->
-          LSet.fold LSet.add (Instance.levels u) s
-    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
-          LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) ->
-      let u = Sorts.univ_of_sort u in
-      LSet.fold LSet.add (Universe.levels u) s
-    | _ -> Constr.fold aux s c
-  in aux LSet.empty c
-
-let restrict_universe_context (univs, csts) keep =
-  let removed = LSet.diff univs keep in
-  if LSet.is_empty removed then univs, csts
-  else
-  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
-  let g = UGraph.empty_universes in
-  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
-  let g = UGraph.merge_constraints csts g in
-  let allkept = LSet.diff allunivs removed in
-  let csts = UGraph.constraints_for ~kept:allkept g in
-  (LSet.inter univs keep, csts)
+let restrict_universe_context = UState.restrict_universe_context
diff --git a/engine/univops.mli b/engine/univops.mli
index 57a53597b9..597d2d6785 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -13,9 +13,7 @@ open Univ
 
 (** Return the set of all universes appearing in [constr]. *)
 val universes_of_constr : constr -> LSet.t
+[@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
-   the universes in [keep]. The constraints [csts] are adjusted so
-   that transitive constraints between remaining universes (those in
-   [keep] and those not in [univs]) are preserved. *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+[@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c97969c0e0..b490aa5092 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -227,6 +227,12 @@ let mkMeta  n =  Meta n
 (* Constructs a Variable named id *)
 let mkVar id = Var id
 
+let mkRef (gr,u) = let open GlobRef in match gr with
+  | ConstRef c -> mkConstU (c,u)
+  | IndRef ind -> mkIndU (ind,u)
+  | ConstructRef c -> mkConstructU (c,u)
+  | VarRef x -> mkVar x
+
 (************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
 (************************************************************************)
@@ -401,6 +407,12 @@ let destCoFix c = match kind c with
   | CoFix cofix -> cofix
   | _ -> raise DestKO
 
+let destRef c = let open GlobRef in match kind c with
+  | Var x -> VarRef x, Univ.Instance.empty
+  | Const (c,u) -> ConstRef c, u
+  | Ind (ind,u) -> IndRef ind, u
+  | Construct (c,u) -> ConstructRef c, u
+  | _ -> raise DestKO
 
 (******************************************************************)
 (* Flattening and unflattening of embedded applications and casts *)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 3c9cc96a0d..c012f04260 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -128,6 +128,9 @@ val mkConstruct : constructor -> constr
 val mkConstructU : pconstructor -> constr
 val mkConstructUi : pinductive * int -> constr
 
+(** Make a constant, inductive, constructor or variable. *)
+val mkRef : GlobRef.t Univ.puniverses -> constr
+
 (** Constructs a destructor of inductive type.
     
     [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
@@ -340,6 +343,8 @@ val destFix : constr -> fixpoint
 
 val destCoFix : constr -> cofixpoint
 
+val destRef : constr -> GlobRef.t Univ.puniverses
+
 (** {6 Equality} *)
 
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2fa33eb1cd..3b7e3ae544 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -419,12 +419,6 @@ let constant_type env (kn,u) =
     let csts = constraints_of cb u in
     (subst_instance_constr u cb.const_type, csts)
 
-let constant_context env kn =
-  let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.AUContext.empty
-  | Polymorphic_const ctx -> ctx
-
 type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
@@ -550,28 +544,38 @@ let lookup_inductive_variables (kn,_i) env =
 let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
 
+(* Universes *)
+let constant_context env c =
+  let cb = lookup_constant c env in
+  Declareops.constant_polymorphic_context cb
+
+let universes_of_global env r =
+  let open GlobRef in
+    match r with
+    | VarRef _ -> Univ.AUContext.empty
+    | ConstRef c -> constant_context env c
+    | IndRef (mind,_) | ConstructRef ((mind,_),_) ->
+      let mib = lookup_mind mind env in
+      Declareops.inductive_polymorphic_context mib
+
 (* Returns the list of global variables in a term *)
 
-let vars_of_global env constr =
-  match kind constr with
-      Var id -> Id.Set.singleton id
-    | Const (kn, _) -> lookup_constant_variables kn env
-    | Ind (ind, _) -> lookup_inductive_variables ind env
-    | Construct (cstr, _) -> lookup_constructor_variables cstr env
-    (** FIXME: is Proj missing? *)
-    | _ -> raise Not_found
+let vars_of_global env gr =
+  let open GlobRef in
+  match gr with
+  | VarRef id -> Id.Set.singleton id
+  | ConstRef kn -> lookup_constant_variables kn env
+  | IndRef ind -> lookup_inductive_variables ind env
+  | ConstructRef cstr -> lookup_constructor_variables cstr env
 
 let global_vars_set env constr =
   let rec filtrec acc c =
-    let acc =
-      match kind c with
-      | Var _ | Const _ | Ind _ | Construct _ ->
-	  Id.Set.union (vars_of_global env c) acc
-      | _ ->
-	  acc in
-    Constr.fold filtrec acc c
+    match destRef c with
+    | gr, _ ->
+      Id.Set.union (vars_of_global env gr) acc
+    | exception DestKO -> Constr.fold filtrec acc c
   in
-    filtrec Id.Set.empty constr
+  filtrec Id.Set.empty constr
 
 
 (* [keep_hyps env ids] keeps the part of the section context of [env] which
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 031e7968d7..3d653bcfe0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -267,6 +267,8 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
 val set_engagement : engagement -> env -> env
 val set_typing_flags : typing_flags -> env -> env
 
+val universes_of_global : env -> GlobRef.t -> AUContext.t
+
 (** {6 Sets of referred section variables }
    [global_vars_set env c] returns the list of [id]'s occurring either
    directly as [Var id] in [c] or indirectly as a section variable
@@ -274,8 +276,7 @@ val set_typing_flags : typing_flags -> env -> env
 
 val global_vars_set : env -> constr -> Id.Set.t
 
-(** the constr must be a global reference *)
-val vars_of_global : env -> constr -> Id.Set.t
+val vars_of_global : env -> GlobRef.t -> Id.Set.t
 
 (** closure of the input id set w.r.t. dependency *)
 val really_needed : env -> Id.Set.t -> Id.Set.t
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7456ecea56..164a47dd9a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -432,21 +432,8 @@ and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
 
-let universe_levels_of_constr _env c =
-  let rec aux s c =
-    match kind c with
-    | Const (_c, u) ->
-       LSet.fold LSet.add (Instance.levels u) s
-    | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
-       LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) ->
-      let u = Sorts.univ_of_sort u in
-      LSet.fold LSet.add (Universe.levels u) s
-    | _ -> Constr.fold aux s c
-  in aux LSet.empty c
-
 let check_wellformed_universes env c =
-  let univs = universe_levels_of_constr env c in
+  let univs = universes_of_constr c in
   try UGraph.check_declared_universes (universes env) univs
   with UGraph.UndeclaredLevel u ->
     error_undeclared_universe env u
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fa37834a23..d09b54e7ec 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1065,6 +1065,9 @@ type universe_context_set = ContextSet.t
 type 'a in_universe_context = 'a * universe_context
 type 'a in_universe_context_set = 'a * universe_context_set
 
+let extend_in_context_set (a, ctx) ctx' =
+  (a, ContextSet.union ctx ctx')
+
 (** Substitutions. *)
 
 let empty_subst = LMap.empty
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1aa53b8aa8..7ac8247ca4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -433,6 +433,9 @@ end
 type 'a in_universe_context = 'a * UContext.t
 type 'a in_universe_context_set = 'a * ContextSet.t
 
+val extend_in_context_set : 'a in_universe_context_set -> ContextSet.t ->
+  'a in_universe_context_set
+
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 9d5d79124b..7380a860dd 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -312,3 +312,17 @@ let subst_instance_constr subst c =
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
   else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
+
+let universes_of_constr c =
+  let open Univ in
+  let rec aux s c =
+    match kind c with
+    | Const (_c, u) ->
+       LSet.fold LSet.add (Instance.levels u) s
+    | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
+       LSet.fold LSet.add (Instance.levels u) s
+    | Sort u when not (Sorts.is_small u) ->
+      let u = Sorts.univ_of_sort u in
+      LSet.fold LSet.add (Universe.levels u) s
+    | _ -> Constr.fold aux s c
+  in aux LSet.empty c
diff --git a/kernel/vars.mli b/kernel/vars.mli
index fdddbdb342..7c928e2694 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -139,3 +139,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Instance.t -> constr -> constr
 val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context
+
+val universes_of_constr : constr -> Univ.LSet.t
diff --git a/library/global.ml b/library/global.ml
index 769a4bea38..1ad72afea1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -210,20 +210,6 @@ let type_of_global_in_context env r =
     let inst = Univ.make_abstract_instance univs in
     Inductive.type_of_constructor (cstr,inst) specif, univs
 
-let universes_of_global env r = 
-    match r with
-    | VarRef id -> Univ.AUContext.empty
-    | ConstRef c -> 
-      let cb = Environ.lookup_constant c env in 
-      Declareops.constant_polymorphic_context cb
-    | IndRef ind ->
-      let (mib, oib) = Inductive.lookup_mind_specif env ind in
-      Declareops.inductive_polymorphic_context mib
-    | ConstructRef cstr ->
-      let (mib,oib) = 
-        Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-      Declareops.inductive_polymorphic_context mib
-
 let universes_of_global gr = 
   universes_of_global (env ()) gr
 
diff --git a/library/global.mli b/library/global.mli
index fd6c9a60d4..29255a70ff 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -143,6 +143,7 @@ val type_of_global_in_context : Environ.env ->
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
 val universes_of_global : GlobRef.t -> Univ.AUContext.t
+[@@ocaml.deprecated "Use [Environ.universes_of_global]"]
 
 (** {6 Retroknowledge } *)
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9ca91d62da..d57b931785 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -676,11 +676,15 @@ let build_case_scheme fa =
 (*   in  *)
   let funs =
     let (_,f,_) = fa in
-    try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
+    try (let open GlobRef in
+         match Smartlocate.global_with_alias f with
+         | ConstRef c -> c
+         | IndRef _ | ConstructRef _ | VarRef _ -> assert false)
     with Not_found ->
       user_err ~hdr:"FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_qualid f) in
-  let first_fun,u = destConst  funs in
+  let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
+  let first_fun = funs in
   let funs_mp = Constant.modpath first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
   let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
@@ -688,7 +692,7 @@ let build_case_scheme fa =
   let prop_sort = InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
+    List.assoc_f Constant.equal funs this_block_funs_indexes
   in
   let (ind, sf) =
 	 let ind = first_fun_kn,funs_indexes in
@@ -700,7 +704,7 @@ let build_case_scheme fa =
   let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
-       UnivGen.new_sort_in_family x
+       fst @@ UnivGen.fresh_sort_in_family x
     )
       fa
   in
@@ -718,7 +722,7 @@ let build_case_scheme fa =
       (Some princ_name)
       this_block_funs
       0
-      (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|])
+      (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|])
   in
   ()
  
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9fa333c629..ca3160f4c4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -24,6 +24,7 @@ open Globnames
 open Nameops
 open CErrors
 open Util
+open UnivGen
 open Tacticals
 open Tacmach
 open Tactics
@@ -50,7 +51,7 @@ open Context.Rel.Declaration
 (* Ugly things which should not be here *)
 
 [@@@ocaml.warning "-3"]
-let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ constr_of_global @@
   Coqlib.find_reference "RecursiveDefinition" m s
 
 let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
@@ -62,7 +63,7 @@ let pr_leconstr_rd =
 
 let coq_init_constant s =
   EConstr.of_constr (
-    UnivGen.constr_of_global @@
+    constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 [@@@ocaml.warning "+3"]
 
@@ -96,9 +97,6 @@ let type_of_const sigma t =
       Typeops.type_of_constant_in (Global.env()) (sp, u)
     |_ -> assert false
 
-let 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)
 
 let const_of_ref = function
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 85e759d152..9585826109 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+module CVars = Vars
 open Ltac_plugin
 open Pp
 open Util
@@ -150,8 +151,8 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na univs c =
   let open Constr in
-  let vars = Univops.universes_of_constr c in
-  let univs = Univops.restrict_universe_context univs vars in
+  let vars = CVars.universes_of_constr c in
+  let univs = UState.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~univs c),
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 62d719034c..22f438c00c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -457,7 +457,7 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
-        acc2 := Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) !acc2
+        acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
     | _ ->
         iter_with_full_binders sigma
           (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 495f5c0660..f2881e4a19 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -405,32 +405,25 @@ let interp_glob_level ?loc evd : glob_level -> _ = function
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_level_info ?loc evd s
 
-let interp_instance ?loc evd ~len l =
-  if len != List.length l then
+let interp_instance ?loc evd l =
+  let evd, l' =
+    List.fold_left
+      (fun (evd, univs) l ->
+         let evd, l = interp_glob_level ?loc evd l in
+         (evd, l :: univs)) (evd, [])
+      l
+  in
+  if List.exists (fun l -> Univ.Level.is_prop l) l' then
     user_err ?loc ~hdr:"pretype"
-      (str "Universe instance should have length " ++ int len)
-  else
-    let evd, l' =
-      List.fold_left
-        (fun (evd, univs) l ->
-	  let evd, l = interp_glob_level ?loc evd l in
-	  (evd, l :: univs)) (evd, [])
-        l
-    in
-    if List.exists (fun l -> Univ.Level.is_prop l) l' then
-      user_err ?loc ~hdr:"pretype"
-	(str "Universe instances cannot contain Prop, polymorphic" ++
-	   str " universe instances must be greater or equal to Set.");
-    evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+      (str "Universe instances cannot contain Prop, polymorphic" ++
+       str " universe instances must be greater or equal to Set.");
+  evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
 
 let pretype_global ?loc rigid env evd gr us = 
   let evd, instance = 
     match us with
     | None -> evd, None
-    | Some l -> 
-       let _, ctx = Global.constr_of_global_in_context !!env gr in
-       let len = Univ.AUContext.size ctx in
-       interp_instance ?loc evd ~len l
+    | Some l -> interp_instance ?loc evd l
   in
   Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7e5815acd1..ce12aaeeb0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -320,7 +320,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 = UnivGen.constr_of_global_univ (glob, inst) in
+  let term = Constr.mkRef (glob, inst) in
     (*FIXME subclasses should now get substituted for each particular instance of
       the polymorphic superclass *)
     aux pri term ty [glob]
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index de151fb6e5..25cf789193 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -347,8 +347,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
           not (Safe_typing.empty_private_constants = eff))
         in
         let typ = if allow_deferred then t else nf t in
-        let used_univs_body = Univops.universes_of_constr body in
-        let used_univs_typ = Univops.universes_of_constr typ in
+        let used_univs_body = Vars.universes_of_constr body in
+        let used_univs_typ = Vars.universes_of_constr typ in
         if allow_deferred then
           let initunivs = UState.const_univ_entry ~poly initial_euctx in
           let ctx = constrain_variables universes in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 16b94cd154..b12018cd66 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -785,7 +785,7 @@ let build_congr env (eq,refl,ctx) ind =
   let varH = fresh env (Id.of_string "H") in
   let varf = fresh env (Id.of_string "f") in
   let ci = make_case_info (Global.env()) ind RegularStyle in
-  let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in
+  let uni, ctx = Univ.extend_in_context_set (UnivGen.new_global_univ ()) ctx in
   let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in
   let c = 
   my_it_mkLambda_or_LetIn paramsctxt
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3e3ef78c5d..c4a6b1605d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1792,7 +1792,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
         let u = EInstance.kind sigma u in
-        let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
+        let eq = Constr.mkRef (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
         | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
@@ -1843,7 +1843,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
     try
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
       let u = EInstance.kind sigma u in
-      let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
+      let eq = Constr.mkRef (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
       if EConstr.eq_constr sigma x y then failwith "caught";
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 245bdce5ad..0c10f32c86 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -787,7 +787,7 @@ let secvars_of_constr env sigma c =
   secvars_of_idset (Termops.global_vars_set env sigma c)
 
 let secvars_of_global env gr =
-  secvars_of_idset (vars_of_global_reference env gr)
+  secvars_of_idset (vars_of_global env gr)
 
 let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env sigma c in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 09e2b8df45..3cf5e9bfdf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 (*i*)
+module CVars = Vars
 open Names
 open EConstr
 open Nametab
@@ -116,8 +117,8 @@ let instance_hook k info global imps ?hook cst =
 let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
   let kind = IsDefinition Instance in
   let sigma =
-    let levels = Univ.LSet.union (Univops.universes_of_constr termtype)
-                                 (Univops.universes_of_constr term) in
+    let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
+                                 (CVars.universes_of_constr term) in
     Evd.restrict_universe_context sigma levels
   in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 9497f2fb03..e990f0cd15 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -162,7 +162,7 @@ let do_assumptions kind nl l =
   let nf_evar c = EConstr.to_constr sigma c in
   let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
       let t = nf_evar t in
-      let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
+      let uvars = Univ.LSet.union uvars (Vars.universes_of_constr t) in
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
@@ -173,7 +173,7 @@ let do_assumptions kind nl l =
       let t = replace_vars subst t in
       let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
       let subst' = List.map2
-          (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u)))
+          (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
       in
       subst'@subst, status' && status, next_uctx uctx)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 5f340dc144..138696e3a7 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -266,7 +266,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let env = Global.env() in
     let indexes = search_guard env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-    let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+    let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
@@ -299,7 +299,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let vars = Univops.universes_of_constr (List.hd fixdecls) in
+    let vars = Vars.universes_of_constr (List.hd fixdecls) in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5352cf5f8c..0ac97a74e4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -487,8 +487,8 @@ let declare_definition prg =
   let typ = nf typ in
   let body = nf body in
   let uvars = Univ.LSet.union
-      (Univops.universes_of_constr typ)
-      (Univops.universes_of_constr body) in
+      (Vars.universes_of_constr typ)
+      (Vars.universes_of_constr body) in
   let uctx = UState.restrict prg.prg_ctx uvars in
   let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
   let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in