Split off Universes functions dealing with generating new universes.

44 files changed, 533 insertions, 396 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 207dbde1e..512908e13 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,4 +1,5 @@
 UnivNames
+UnivGen
 Universes
 Univops
 UState
diff --git a/engine/evd.ml b/engine/evd.ml
index 20a7c80ea..b2b8e7ccc 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -804,19 +804,19 @@ let make_flexible_variable evd ~algebraic u =
 (****************************************)
 
 let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
-  with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s)
+  with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s)
 
 let fresh_constant_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
 
 let fresh_inductive_instance ?loc env evd i =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i)
+  with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i)
 
 let fresh_constructor_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env 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 (Universes.fresh_global_instance ?names env gr)
+  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
 
 let whd_sort_variable evd t = t
 
diff --git a/engine/uState.ml b/engine/uState.ml
index ffb54d441..839bb5ae9 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -471,7 +471,7 @@ let emit_side_effects eff u =
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = Universes.new_univ_level () in
+  let u = UnivGen.new_univ_level () in
   let ctx' = Univ.ContextSet.add_universe u ctx in
   let uctx', pred =
     match rigid with
@@ -582,7 +582,7 @@ let fix_undefined_variables uctx =
     uctx_univ_algebraic = algs' }
 
 let refresh_undefined_univ_variables uctx =
-  let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
+  let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in
   let subst_fn u = Univ.subst_univs_level_level subst u in
   let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc)
     uctx.uctx_univ_algebraic Univ.LSet.empty 
diff --git a/engine/univGen.ml b/engine/univGen.ml
new file mode 100644
index 000000000..796a1bcc1
--- /dev/null
+++ b/engine/univGen.ml
@@ -0,0 +1,246 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Sorts
+open Names
+open Constr
+open Environ
+open Univ
+
+(* Generator of levels *)
+type universe_id = DirPath.t * int
+
+let new_univ_id, set_remote_new_univ_id =
+  RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
+    ~build:(fun n -> Global.current_dirpath (), n)
+
+let new_univ_level () =
+  let dp, id = new_univ_id () in
+  Univ.Level.make dp id
+
+let fresh_level () = new_univ_level ()
+
+(* TODO: remove *)
+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_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 () =
+    let len1 = Array.length (Instance.to_array inst)
+    and len2 = AUContext.size ctx 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)
+      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)
+
+(** Fresh universe polymorphic construction *)
+
+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)
+
+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_constant_instance env sp =
+  fresh_constant_instance env sp None
+
+let fresh_inductive_instance env sp =
+  fresh_inductive_instance env sp None
+
+let fresh_constructor_instance env sp =
+  fresh_constructor_instance env sp None
+
+let constr_of_global gr =
+  let c, ctx = fresh_global_instance (Global.env ()) gr in
+    if not (Univ.ContextSet.is_empty ctx) then
+      if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
+        (* Should be an error as we might forget constraints, allow for now
+           to make firstorder work with "using" clauses *)
+        c
+      else CErrors.user_err ~hdr:"constr_of_global"
+          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty 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 fresh_global_or_constr_instance env = function
+  | IsConstr c -> c, ContextSet.empty
+  | IsGlobal gr -> fresh_global_instance env gr
+
+let global_of_constr c =
+  match kind c with
+  | Const (c, u) -> ConstRef c, u
+  | Ind (i, u) -> IndRef i, u
+  | Construct (c, u) -> ConstructRef c, u
+  | Var id -> VarRef id, Instance.empty
+  | _ -> raise Not_found
+
+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
+  | 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 type_of_global t = type_of_reference (Global.env ()) t
+
+let fresh_sort_in_family env = function
+  | InProp -> Sorts.prop, ContextSet.empty
+  | InSet -> Sorts.set, ContextSet.empty
+  | InType ->
+    let u = fresh_level () in
+      Type (Univ.Universe.make u), ContextSet.singleton u
+
+let new_sort_in_family sf =
+  fst (fresh_sort_in_family (Global.env ()) sf)
+
+let extend_context (a, ctx) (ctx') =
+  (a, ContextSet.union ctx ctx')
+
+let new_global_univ () =
+  let u = fresh_level () in
+  (Univ.Universe.make u, ContextSet.singleton u)
+
+let fresh_universe_context_set_instance ctx =
+  if ContextSet.is_empty ctx then LMap.empty, ctx
+  else
+    let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
+    let univs',subst = LSet.fold
+      (fun u (univs',subst) ->
+        let u' = fresh_level () in
+          (LSet.add u' univs', LMap.add u u' subst))
+      univs (LSet.empty, LMap.empty)
+    in
+    let cst' = subst_univs_level_constraints subst cst in
+      subst, (univs', cst')
diff --git a/engine/univGen.mli b/engine/univGen.mli
new file mode 100644
index 000000000..8169dbda4
--- /dev/null
+++ b/engine/univGen.mli
@@ -0,0 +1,80 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Constr
+open Environ
+open Univ
+
+
+(** The global universe counter *)
+type universe_id = DirPath.t * int
+
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
+
+(** Side-effecting functions creating new universe levels. *)
+
+val new_univ_id : unit -> universe_id
+val new_univ_level : unit -> Level.t
+val new_univ : unit -> Universe.t
+val new_Type : unit -> types
+val new_Type_sort : unit -> Sorts.t
+
+val new_global_univ : unit -> Universe.t in_universe_context_set
+val new_sort_in_family : Sorts.family -> Sorts.t
+
+(** 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_from : AUContext.t -> Instance.t option ->
+  Instance.t in_universe_context_set
+
+val fresh_sort_in_family : env -> Sorts.family ->
+  Sorts.t in_universe_context_set
+val fresh_constant_instance : env -> Constant.t ->
+  pconstant in_universe_context_set
+val fresh_inductive_instance : env -> inductive ->
+  pinductive in_universe_context_set
+val fresh_constructor_instance : env -> constructor ->
+  pconstructor in_universe_context_set
+
+val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+  constr in_universe_context_set
+
+val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
+  constr in_universe_context_set
+
+(** Get fresh variables for the universe context.
+    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
+val fresh_universe_context_set_instance : ContextSet.t ->
+  universe_level_subst * ContextSet.t
+
+(** Raises [Not_found] if not a global reference. *)
+val global_of_constr : constr -> GlobRef.t puniverses
+
+val constr_of_global_univ : GlobRef.t puniverses -> constr
+
+val extend_context : 'a in_universe_context_set -> ContextSet.t ->
+  'a in_universe_context_set
+
+(** Create a fresh global in the global environment, without side effects.
+    BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
+    the constraints should be properly added to an evd.
+    See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
+    the proper way to get a fresh copy of a global reference. *)
+val constr_of_global : GlobRef.t -> constr
+
+(** 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 : GlobRef.t -> types in_universe_context_set
diff --git a/engine/universes.ml b/engine/universes.ml
index 1dccde025..29c9bd017 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -11,9 +11,7 @@
 open Sorts
 open Util
 open Pp
-open Names
 open Constr
-open Environ
 open Univ
 
 (* To disallow minimization to Set *)
@@ -214,226 +212,6 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
   let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in
   if res then Some !cstrs else None
 
-(* Generator of levels *)
-type universe_id = DirPath.t * int
-
-let new_univ_id, set_remote_new_univ_id =
-  RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Global.current_dirpath (), n)
-
-let new_univ_level () =
-  let dp, id = new_univ_id () in
-  Univ.Level.make dp id
-
-let fresh_level () = new_univ_level ()
-
-(* TODO: remove *)
-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_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 () = 
-    let len1 = Array.length (Instance.to_array inst)
-    and len2 = AUContext.size ctx in
-      if not (len1 == len2) then
-	CErrors.user_err ~hdr:"Universes"
-	  (str "Polymorphic constant expected " ++ int len2 ++ 
-	     str" levels but was given " ++ int len1)
-      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)
-
-(** Fresh universe polymorphic construction *)
-
-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)
-
-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_constant_instance env sp = 
-  fresh_constant_instance env sp None
-
-let fresh_inductive_instance env sp = 
-  fresh_inductive_instance env sp None
-
-let fresh_constructor_instance env sp = 
-  fresh_constructor_instance env sp None
-
-let constr_of_global gr =
-  let c, ctx = fresh_global_instance (Global.env ()) gr in
-    if not (Univ.ContextSet.is_empty ctx) then
-      if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then 
-	(* Should be an error as we might forget constraints, allow for now
-	   to make firstorder work with "using" clauses *)
-	c
-      else CErrors.user_err ~hdr:"constr_of_global"
-          Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
-	      str " would forget universes.")
-    else c
-
-let constr_of_reference = constr_of_global
-
-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 fresh_global_or_constr_instance env = function
-  | IsConstr c -> c, ContextSet.empty
-  | IsGlobal gr -> fresh_global_instance env gr
-
-let global_of_constr c =
-  match kind c with
-  | Const (c, u) -> ConstRef c, u
-  | Ind (i, u) -> IndRef i, u
-  | Construct (c, u) -> ConstructRef c, u
-  | Var id -> VarRef id, Instance.empty
-  | _ -> raise Not_found
-
-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
-  | 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 type_of_global t = type_of_reference (Global.env ()) t
-
-let fresh_sort_in_family env = function
-  | InProp -> Sorts.prop, ContextSet.empty
-  | InSet -> Sorts.set, ContextSet.empty
-  | InType -> 
-    let u = fresh_level () in
-      Type (Univ.Universe.make u), ContextSet.singleton u
-
-let new_sort_in_family sf =
-  fst (fresh_sort_in_family (Global.env ()) sf)
-
-let extend_context (a, ctx) (ctx') =
-  (a, ContextSet.union ctx ctx')
-
-let new_global_univ () =
-  let u = fresh_level () in
-    (Univ.Universe.make u, ContextSet.singleton u)
-
 (** Simplification *)
 
 let add_list_map u t map =
@@ -504,19 +282,6 @@ let subst_univs_constr =
       CProfile.profile2 subst_univs_constr_key subst_univs_constr
   else subst_univs_constr
 
-let fresh_universe_context_set_instance ctx =
-  if ContextSet.is_empty ctx then LMap.empty, ctx
-  else
-    let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
-    let univs',subst = LSet.fold
-      (fun u (univs',subst) ->
-	let u' = fresh_level () in
-	  (LSet.add u' univs', LMap.add u u' subst))
-      univs (LSet.empty, LMap.empty)
-    in
-    let cst' = subst_univs_level_constraints subst cst in
-      subst, (univs', cst')
-
 let normalize_univ_variable ~find =
   let rec aux cur =
     let b = find cur in
@@ -1020,6 +785,8 @@ let solve_constraints_system levels level_bounds level_min =
   v
 
 (** Deprecated *)
+
+(** UnivNames *)
 type universe_binders = UnivNames.universe_binders
 type univ_name_list = UnivNames.univ_name_list
 
@@ -1036,3 +803,30 @@ let register_universe_binders = UnivNames.register_universe_binders
 let universe_binders_of_global = UnivNames.universe_binders_of_global
 
 let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names
+
+(** UnivGen *)
+type universe_id = UnivGen.universe_id
+
+let set_remote_new_univ_id = UnivGen.set_remote_new_univ_id
+let new_univ_id = UnivGen.new_univ_id
+let new_univ_level = UnivGen.new_univ_level
+let new_univ = UnivGen.new_univ
+let new_Type = UnivGen.new_Type
+let new_Type_sort = UnivGen.new_Type_sort
+let new_global_univ = UnivGen.new_global_univ
+let new_sort_in_family = UnivGen.new_sort_in_family
+let fresh_instance_from_context = UnivGen.fresh_instance_from_context
+let fresh_instance_from = UnivGen.fresh_instance_from
+let fresh_sort_in_family = UnivGen.fresh_sort_in_family
+let fresh_constant_instance = UnivGen.fresh_constant_instance
+let fresh_inductive_instance = UnivGen.fresh_inductive_instance
+let fresh_constructor_instance = UnivGen.fresh_constructor_instance
+let fresh_global_instance = UnivGen.fresh_global_instance
+let fresh_global_or_constr_instance = UnivGen.fresh_global_or_constr_instance
+let fresh_universe_context_set_instance = UnivGen.fresh_universe_context_set_instance
+let global_of_constr = UnivGen.global_of_constr
+let constr_of_global_univ = UnivGen.constr_of_global_univ
+let extend_context = UnivGen.extend_context
+let constr_of_global = UnivGen.constr_of_global
+let constr_of_reference = UnivGen.constr_of_global
+let type_of_global = UnivGen.type_of_global
diff --git a/engine/universes.mli b/engine/universes.mli
index aaf295c1d..da4a00751 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -19,22 +19,6 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
 
 (** Universes *)
 
-(** The global universe counter *)
-type universe_id = DirPath.t * int
-
-val set_remote_new_univ_id : universe_id RemoteCounter.installer
-
-(** Side-effecting functions creating new universe levels. *)
-
-val new_univ_id : unit -> universe_id
-val new_univ_level : unit -> Level.t
-val new_univ : unit -> Universe.t
-val new_Type : unit -> types
-val new_Type_sort : unit -> Sorts.t
-
-val new_global_univ : unit -> Universe.t in_universe_context_set
-val new_sort_in_family : Sorts.family -> Sorts.t
-
 (** {6 Constraints for type inference}
 
     When doing conversion of universes, not only do we have =/<= constraints but
@@ -82,43 +66,6 @@ val eq_constr_univs_infer_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
 
-(** 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_from : AUContext.t -> Instance.t option ->
-  Instance.t in_universe_context_set
-
-val fresh_sort_in_family : env -> Sorts.family -> 
-  Sorts.t in_universe_context_set
-val fresh_constant_instance : env -> Constant.t ->
-  pconstant in_universe_context_set
-val fresh_inductive_instance : env -> inductive ->
-  pinductive in_universe_context_set
-val fresh_constructor_instance : env -> constructor ->
-  pconstructor in_universe_context_set
-
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
-  constr in_universe_context_set
-
-val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> 
-  constr in_universe_context_set
-
-(** Get fresh variables for the universe context.
-    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : ContextSet.t -> 
-  universe_level_subst * ContextSet.t
-
-(** Raises [Not_found] if not a global reference. *)
-val global_of_constr : constr -> GlobRef.t puniverses
-
-val constr_of_global_univ : GlobRef.t puniverses -> constr
-
-val extend_context : 'a in_universe_context_set -> ContextSet.t -> 
-  'a in_universe_context_set
-
 (** Simplification and pruning of constraints:
     [normalize_context_set ctx us]
 
@@ -166,22 +113,6 @@ val normalize_universe_opt_subst : universe_opt_subst ->
 val normalize_universe_subst : universe_subst ->
   (Universe.t -> Universe.t)
 
-(** Create a fresh global in the global environment, without side effects.
-    BEWARE: this raises an ANOMALY on polymorphic constants/inductives: 
-    the constraints should be properly added to an evd. 
-    See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
-    the proper way to get a fresh copy of a global reference. *)
-val constr_of_global : GlobRef.t -> constr
-
-(** ** DEPRECATED ** synonym of [constr_of_global] *)
-val constr_of_reference : GlobRef.t -> constr
-[@@ocaml.deprecated "synonym of [constr_of_global]"]
-
-(** 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 : GlobRef.t -> types in_universe_context_set
-
 (** Full universes substitutions into terms *)
 
 val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 
@@ -199,6 +130,7 @@ val solve_constraints_system : Universe.t option array -> Universe.t array -> Un
   Universe.t array
 
 (** *********************************** Deprecated *)
+
 [@@@ocaml.warning "-3"]
 val set_minimization : bool ref
 [@@ocaml.deprecated "Becoming internal."]
@@ -235,3 +167,87 @@ type univ_name_list = UnivNames.univ_name_list
 val universe_binders_with_opt_names : Globnames.global_reference ->
   Univ.Level.t list -> univ_name_list option -> universe_binders
 [@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"]
+
+(** ****** Deprecated: moved to [UnivGen] *)
+
+type universe_id = UnivGen.universe_id
+[@@ocaml.deprecated "Use [UnivGen.universe_id]"]
+
+val set_remote_new_univ_id : universe_id RemoteCounter.installer
+[@@ocaml.deprecated "Use [UnivGen.set_remote_new_univ_id]"]
+
+val new_univ_id : unit -> universe_id
+[@@ocaml.deprecated "Use [UnivGen.new_univ_id]"]
+
+val new_univ_level : unit -> Level.t
+[@@ocaml.deprecated "Use [UnivGen.new_univ_level]"]
+
+val new_univ : unit -> Universe.t
+[@@ocaml.deprecated "Use [UnivGen.new_univ]"]
+
+val new_Type : unit -> types
+[@@ocaml.deprecated "Use [UnivGen.new_Type]"]
+
+val new_Type_sort : unit -> Sorts.t
+[@@ocaml.deprecated "Use [UnivGen.new_Type_sort]"]
+
+val new_global_univ : unit -> Universe.t in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.new_global_univ]"]
+
+val new_sort_in_family : Sorts.family -> Sorts.t
+[@@ocaml.deprecated "Use [UnivGen.new_sort_in_family]"]
+
+val fresh_instance_from_context : AUContext.t ->
+  Instance.t constrained
+[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from_context]"]
+
+val fresh_instance_from : AUContext.t -> Instance.t option ->
+  Instance.t in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"]
+
+val fresh_sort_in_family : env -> Sorts.family ->
+  Sorts.t in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"]
+
+val fresh_constant_instance : env -> Constant.t ->
+  pconstant in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_constant_instance]"]
+
+val fresh_inductive_instance : env -> inductive ->
+  pinductive in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_inductive_instance]"]
+
+val fresh_constructor_instance : env -> constructor ->
+  pconstructor in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_constructor_instance]"]
+
+val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference ->
+  constr in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_global_instance]"]
+
+val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
+  constr in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.fresh_global_or_constr_instance]"]
+
+val fresh_universe_context_set_instance : ContextSet.t ->
+  universe_level_subst * ContextSet.t
+[@@ocaml.deprecated "Use [UnivGen.fresh_universe_context_set_instance]"]
+
+val global_of_constr : constr -> Globnames.global_reference puniverses
+[@@ocaml.deprecated "Use [UnivGen.global_of_constr]"]
+
+val constr_of_global_univ : Globnames.global_reference puniverses -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global_univ]"]
+
+val extend_context : 'a in_universe_context_set -> ContextSet.t ->
+  'a in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.extend_context]"]
+
+val constr_of_global : Globnames.global_reference -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"]
+
+val constr_of_reference : Globnames.global_reference -> constr
+[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"]
+
+val type_of_global : Globnames.global_reference -> types in_universe_context_set
+[@@ocaml.deprecated "Use [UnivGen.type_of_global]"]
diff --git a/interp/declare.ml b/interp/declare.ml
index 34bf5c8a2..bc2d2068a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -564,7 +564,7 @@ let do_universe poly l =
   in
   let l =
     List.map (fun {CAst.v=id} ->
-      let lev = Universes.new_univ_id () in
+      let lev = UnivGen.new_univ_id () in
       (id, lev)) l
   in
   let src = if poly then BoundUniv else UnqualifiedUniv in
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index a09abfa19..7f98ed427 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -2,11 +2,11 @@ let contrib_name = "btauto"
 
 let init_constant dir s =
   let find_constant contrib dir s =
-    Universes.constr_of_global (Coqlib.find_reference contrib dir s)
+    UnivGen.constr_of_global (Coqlib.find_reference contrib dir s)
   in
   find_constant contrib_name dir s
 
-let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s)
+let get_constant dir s = lazy (UnivGen.constr_of_global @@ Coqlib.coq_reference contrib_name dir s)
 
 let get_inductive dir s =
   let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f25f63624..cdd698304 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -431,7 +431,7 @@ and extract_really_ind env kn mib =
     let packets =
       Array.mapi
 	(fun i mip ->
-	   let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in
+           let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in
 	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
            let ar = EConstr.of_constr ar in
            let info = (fst (flag_of_type env sg ar) = Info) in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 2d7a3e37b..b13580bc0 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -233,7 +233,7 @@ let ll_forall_tac prod backtrack id continue seq=
 
 (* special for compatibility with old Intuition *)
 
-let constant str = Universes.constr_of_global
+let constant str = UnivGen.constr_of_global
   @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 0ea70c19f..96be1d893 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -283,15 +283,15 @@ let fourier_lineq lineq1 =
 let get = Lazy.force
 let cget = get
 let eget c = EConstr.of_constr (Lazy.force c)
-let constant path s = Universes.constr_of_global @@
+let constant path s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "Fourier" path s
 
 (* Standard library *)
 open Coqlib
 let coq_sym_eqT = lazy (build_coq_eq_sym ())
-let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ())
-let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ())
-let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ())
+let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ())
+let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ())
+let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ())
 
 (* Rdefinitions *)
 let constant_real = constant ["Reals";"Rdefinitions"]
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 44fa0740d..3801fec4b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
 
 let rec_pte_id = Id.of_string "Hrec"
 let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
-  let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in
-  let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in
-  let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in
+  let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ()) in
+  let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in
+  let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in
   let rec scan_type  context type_of_hyp : tactic =
     if isLetIn sigma type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
@@ -1603,7 +1603,7 @@ let prove_principle_for_gen
     match !tcc_lemma_ref with
      | Undefined -> user_err Pp.(str "No tcc proof !!")
      | Value lemma -> EConstr.of_constr lemma
-     | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ())
+     | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ())
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index dc0f240bd..a158fc8ff 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -689,7 +689,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) ->
-       Universes.new_sort_in_family x
+       UnivGen.new_sort_in_family x
     )
       fa
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a0b9217c7..35c3acd41 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -117,7 +117,7 @@ let def_of_const t =
     |_ -> assert false
 
 let coq_constant s =
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
@@ -471,7 +471,7 @@ let jmeq () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
-    Universes.constr_of_global @@
+    UnivGen.constr_of_global @@
       Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
@@ -479,7 +479,7 @@ let jmeq_refl () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     EConstr.of_constr @@
-    Universes.constr_of_global @@
+    UnivGen.constr_of_global @@
       Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
   with e when CErrors.noncritical e -> raise (ToShow e)
 
@@ -492,7 +492,7 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded"
 let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
 let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
 
-let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@
+let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@
     Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 094f54156..180952635 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
 let make_eq () =
   try
-    EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
+    EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ()))
   with _ -> assert false 
 
 	  
@@ -512,7 +512,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
 			    intros_with_rewrite
 			  ] g
 			end
-		  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
+                  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENLIST[
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2a3a85fcc..2464c595f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -49,7 +49,7 @@ open Context.Rel.Declaration
 
 (* Ugly things which should not be here *)
 
-let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@
   Coqlib.coq_reference "RecursiveDefinition" m s
 
 let arith_Nat = ["Arith";"PeanoNat";"Nat"]
@@ -61,7 +61,7 @@ let pr_leconstr_rd =
 
 let coq_init_constant s =
   EConstr.of_constr (
-    Universes.constr_of_global @@
+    UnivGen.constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 
 let find_reference sl s =
@@ -1241,7 +1241,7 @@ let get_current_subgoals_types () =
 
 exception EmptySubgoals
 let build_and_l sigma l =
-  let and_constr =  Universes.constr_of_global @@ Coqlib.build_coq_and () in
+  let and_constr =  UnivGen.constr_of_global @@ Coqlib.build_coq_and () in
   let conj_constr = coq_conj () in
   let mk_and p1 p2 =
     mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 168105e8f..4c0357dd8 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -373,7 +373,7 @@ struct
     * ZMicromega.v
     *)
 
-  let gen_constant_in_modules s m n = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
+  let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
   let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
   let constant = gen_constant_in_modules "ZMicromega" coq_modules
   let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 81b44ffad..d2d4639d2 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -136,7 +136,7 @@ let mul = function
   | (Const n,q) when eq_num n num_1 -> q
   | (p,q) -> Mul(p,q)
 
-let gen_constant msg path s = Universes.constr_of_global @@
+let gen_constant msg path s = UnivGen.constr_of_global @@
   coq_reference msg path s
 
 let tpexpr  = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 51cd665f6..e455ebb28 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -206,7 +206,7 @@ let coq_modules =
   init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
     @ [["Coq"; "omega"; "OmegaLemmas"]]
 
-let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s)
+let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s)
 let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 912429c31..7464b42dc 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -120,7 +120,7 @@ open Proofview.Notations
   the constants are loaded in the environment *)
 
 let constant dir s =
-  EConstr.of_constr @@ Universes.constr_of_global @@
+  EConstr.of_constr @@ UnivGen.constr_of_global @@
     Coqlib.coq_reference "Quote" ("quote"::dir) s
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index ad3afafd8..949cba2db 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -69,19 +69,19 @@ let z_module = [["Coq";"ZArith";"BinInt"]]
 
 let init_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x
 let constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" coq_modules x
 let z_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" z_module x
 let bin_constant x =
   EConstr.of_constr @@
-  Universes.constr_of_global @@
+  UnivGen.constr_of_global @@
   Coqlib.gen_reference_in_modules "Omega" bin_module x
 
 (* Logic *)
@@ -170,7 +170,7 @@ let mk_list univ typ l =
   loop l
 
 let mk_plist =
-  let type1lev = Universes.new_univ_level () in
+  let type1lev = UnivGen.new_univ_level () in
   fun l -> mk_list type1lev EConstr.mkProp l
 
 let mk_list = mk_list Univ.Level.set
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 946b6dff4..8a0f48dc4 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -26,27 +26,27 @@ let step_count = ref 0
 
 let node_count = ref 0
 
-let logic_constant s = Universes.constr_of_global @@
+let logic_constant s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s
 
 let li_False = lazy (destInd (logic_constant "False"))
 let li_and   = lazy (destInd (logic_constant "and"))
 let li_or    = lazy (destInd (logic_constant "or"))
 
-let pos_constant s = Universes.constr_of_global @@
+let pos_constant s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s
 
 let l_xI = lazy (pos_constant "xI")
 let l_xO = lazy (pos_constant "xO")
 let l_xH = lazy (pos_constant "xH")
 
-let store_constant s = Universes.constr_of_global @@
+let store_constant s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s
 
 let l_empty = lazy (store_constant "empty")
 let l_push = lazy (store_constant "push")
 
-let constant s = Universes.constr_of_global @@
+let constant s = UnivGen.constr_of_global @@
   Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s
 
 let l_Reflect = lazy (constant "Reflect")
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 074fcb92e..59ba4b7de 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -105,7 +105,7 @@ let protect_tac_in map id =
 let closed_term t l =
   let open Quote_plugin in
   Proofview.tclEVARMAP >>= fun sigma ->
-  let l = List.map Universes.constr_of_global l in
+  let l = List.map UnivGen.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
   if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
 
@@ -233,7 +233,7 @@ let stdlib_modules =
   ]
 
 let coq_constant c =
-  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
+  lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
 let coq_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
@@ -279,7 +279,7 @@ let plugin_modules =
     ]
 
 let my_constant c =
-  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
+  lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
@@ -927,7 +927,7 @@ let ftheory_to_obj : field_info -> obj =
 let field_equality evd r inv req =
   match EConstr.kind !evd req with
     | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
-        let c = Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr in
+        let c = UnivGen.constr_of_global (Coqlib.build_coq_eq_data()).congr in
         let c = EConstr.of_constr c in
         mkApp(c,[|r;r;inv|])
     | _ ->
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e9e045a53..c0026616d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1221,7 +1221,7 @@ let genclrtac cl cs clr =
       (fun type_err gl ->
          tclTHEN
            (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr
-             (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr))
+             (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr))
            (fun gl -> raise type_err)
            gl))
     (old_cleartac clr)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 7d7655d29..a31022919 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -435,7 +435,7 @@ let lz_setoid_relation =
   | env', srel when env' == env -> srel
   | _ ->
     let srel =
-       try Some (Universes.constr_of_global @@
+       try Some (UnivGen.constr_of_global @@
                    Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation")
        with _ -> None in
     last_srel := (env, srel); srel
@@ -482,7 +482,7 @@ let rwprocess_rule dir rule gl =
           | _ ->
             let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
             EConstr.mkApp (pi2, ra), sigma in
-        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then
+        if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then
          let s, sigma = sr sigma 2 in
          loop (converse_dir d) sigma s a.(1) rs 0
         else
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index afa8a12fc..7dbef01c2 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -316,7 +316,7 @@ let lookup_pattern_path_between env (s,t) =
 
 let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; 
 		     coe_is_identity = b; coe_is_projection = b' } =
-  let subst, ctx = Universes.fresh_universe_context_set_instance ctx in
+  let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in
   let c' = Vars.subst_univs_level_constr subst c 
   and t' = Vars.subst_univs_level_constr subst t in
     (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx
@@ -440,7 +440,7 @@ let cache_coercion env sigma (_, c) =
   let () = add_class c.coercion_target in
   let is, _ = class_info c.coercion_source in
   let it, _ = class_info c.coercion_target in
-  let value, ctx = Universes.fresh_global_instance env c.coercion_type in
+  let value, ctx = UnivGen.fresh_global_instance env c.coercion_type in
   let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in
   let typ = EConstr.Unsafe.to_constr typ in
   let xf =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 49c429458..062136ff5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -49,7 +49,7 @@ let _ = Goptions.declare_bool_option {
 (* XXX: we would like to search for this with late binding
    "data.id.type" etc... *)
 let impossible_default_case () =
-  let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
+  let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
   let (_, u) = Constr.destConst c in
   Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx)
 
@@ -210,7 +210,7 @@ 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 u, ctx' = Universes.fresh_instance_from ctx None in
+  let u, ctx' = UnivGen.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
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 3327c250d..40f4d4ff8 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
     if not (Sorts.List.mem kind (elim_sorts specif)) then
       raise
 	(RecursionSchemeError
-	   (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind)))
+           (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family env kind), pind)))
   in
   let ndepar = mip.mind_nrealdecls + 1 in
 
@@ -550,7 +550,7 @@ let check_arities env listdepkind =
        let kelim = elim_sorts (mibi,mipi) in
        if not (Sorts.List.mem kind kelim) then raise
 	 (RecursionSchemeError
-	  (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family env
+          (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family env
 					      kind),(mind,u))))
        else if Int.List.mem ni ln then raise
 	 (RecursionSchemeError (NotMutualInScheme (mind,mind)))
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a4d447902..7394ad826 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -83,7 +83,7 @@ let declare_reduction_effect funkey f =
 
 (** A function to set the value of the print function *)
 let set_reduction_effect x funkey =
-  let termkey = Universes.constr_of_global x in
+  let termkey = UnivGen.constr_of_global x in
   Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey))
 
 
@@ -705,7 +705,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
     try
       let (cst_mod,cst_sect,_) = Constant.repr3 reference in
       let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
-      let (cst, u), ctx = fresh_constant_instance env cst in
+      let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4386144fe..11cc6c1f0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -281,7 +281,7 @@ 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 inst, ctx = UnivGen.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 ctx in
@@ -321,7 +321,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, inst) in
+  let term = UnivGen.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]
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c1d69dfc5..092bb5c27 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -75,7 +75,7 @@ let pf_ids_set_of_hyps gls =
 let pf_get_new_id id gls =
   next_ident_away id (pf_ids_set_of_hyps gls)
 
-let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
+let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
 let pf_reduction_of_red_expr gls re c =
   let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index b3e1500ae..38fd817da 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,7 +60,7 @@ module Make(T : Task) () = struct
   type request = Request of T.request
 
   type more_data =
-    | MoreDataUnivLevel of Universes.universe_id list
+    | MoreDataUnivLevel of UnivGen.universe_id list
 
   let slave_respond (Request r) =
     let res = T.perform r in
@@ -171,7 +171,7 @@ module Make(T : Task) () = struct
         | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
         | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
     let more_univs n =
-      CList.init n (fun _ -> Universes.new_univ_id ()) in
+      CList.init n (fun _ -> UnivGen.new_univ_id ()) in
 
     let rec kill_if () =
       if not (Worker.is_alive proc) then ()
@@ -310,7 +310,7 @@ module Make(T : Task) () = struct
       Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
     ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x));
     (* We ask master to allocate universe identifiers *)
-    Universes.set_remote_new_univ_id (bufferize (fun () ->
+    UnivGen.set_remote_new_univ_id (bufferize (fun () ->
       marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
       match unmarshal_more_data (Option.get !slave_ic) with
       | MoreDataUnivLevel l -> l));
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 15a24fb37..77fe31415 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -79,7 +79,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
   let clenv, c =
     if poly then
       (** Refresh the instance of the hint *)
-      let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
       let emap c = Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       (** Only metas are mentioning the old universes. *)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c3857e6b8..627ac31f5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
   let try_rewrite dir ctx c tc =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+    let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in
     let c' = Vars.subst_univs_level_constr subst c in
     let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index bbcf8def6..ea5d4719c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -226,7 +226,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
   Refine.refine ~typecheck:false begin fun sigma ->
       let sigma, term, ty =
         if poly then
-          let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+          let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
           let map c = Vars.subst_univs_level_constr subst c in
           let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
           sigma, map c, map t
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2408b8f2b..3df9e3f82 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -89,7 +89,7 @@ let rec prolog l n gl =
 
 let out_term env = function
   | IsConstr (c, _) -> c
-  | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
+  | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr))
 
 let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 477de6452..715686ad0 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -102,7 +102,7 @@ let get_coq_eq ctx =
     let eq = Globnames.destIndRef Coqlib.glob_eq in
     (* Do not force the lazy if they are not defined *)
     let eq, ctx = with_context_set ctx 
-      (Universes.fresh_inductive_instance (Global.env ()) eq) in
+      (UnivGen.fresh_inductive_instance (Global.env ()) eq) in
       mkIndU eq, mkConstructUi (eq,1), ctx
   with Not_found ->
     user_err Pp.(str "eq not found.")
@@ -192,7 +192,7 @@ let get_non_sym_eq_data env (ind,u) =
 (**********************************************************************)
 
 let build_sym_scheme env ind =
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n =
@@ -241,11 +241,11 @@ let sym_scheme_kind =
 let const_of_scheme kind env ind ctx = 
   let sym_scheme, eff = (find_scheme kind ind) in
   let sym, ctx = with_context_set ctx 
-    (Universes.fresh_constant_instance (Global.env()) sym_scheme) in
+    (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
     mkConstU sym, ctx, eff
 
 let build_sym_involutive_scheme env ind =
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
@@ -353,7 +353,7 @@ let sym_involutive_scheme_kind =
 (**********************************************************************)
 
 let build_l2r_rew_scheme dep env ind kind =
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
@@ -392,7 +392,7 @@ let build_l2r_rew_scheme dep env ind kind =
                      rel_vect (nrealargs+4) nrealargs;
                      rel_vect 1 nrealargs;
 		     [|mkRel 1|]]) in
-  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -469,7 +469,7 @@ let build_l2r_rew_scheme dep env ind kind =
 (**********************************************************************)
 
 let build_l2r_forward_rew_scheme dep env ind kind =
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n p =
@@ -495,7 +495,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let realsign_ind_P n aP =
     name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in
-  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -561,7 +561,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
 (**********************************************************************)
 
 let build_r2l_forward_rew_scheme dep env ind kind = 
-  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
     get_non_sym_eq_data env indu in
   let cstr n =
@@ -573,7 +573,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
     name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
-  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
@@ -755,7 +755,7 @@ let rew_r2l_scheme_kind =
 
 let build_congr env (eq,refl,ctx) ind =
   let (ind,u as indu), ctx = with_context_set ctx 
-    (Universes.fresh_inductive_instance env ind) in
+    (UnivGen.fresh_inductive_instance env ind) in
   let (mib,mip) = lookup_mind_specif env ind in
   if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
     error "Not an inductive type with a single constructor.";
@@ -778,7 +778,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 = Universes.extend_context (Universes.new_global_univ ()) ctx in
+  let uni, ctx = UnivGen.extend_context (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 d142e10a4..8904cd170 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1781,7 +1781,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 = Universes.constr_of_global_univ (lbeq.eq,u) in
+        let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
         | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
@@ -1832,7 +1832,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 = Universes.constr_of_global_univ (lbeq.eq,u) in
+      let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
       if EConstr.eq_constr sigma x y then failwith "caught";
diff --git a/tactics/hints.ml b/tactics/hints.ml
index d02bab186..39034a19b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -876,7 +876,7 @@ let fresh_global_or_constr env sigma poly cr =
   let isgr, (c, ctx) =
     match cr with
     | IsGlobRef gr ->
-      let (c, ctx) = Universes.fresh_global_instance env gr in
+      let (c, ctx) = UnivGen.fresh_global_instance env gr in
        true, (EConstr.of_constr c, ctx)
     | IsConstr (c, ctx) -> false, (c, ctx)
   in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5e602289b..2a41a50dd 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -59,15 +59,15 @@ exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
 exception NoDecidabilityCoInductive
 
-let constr_of_global g = lazy (Universes.constr_of_global g)
+let constr_of_global g = lazy (UnivGen.constr_of_global g)
 
 (* Some pre declaration of constant we are going to use *)
 let bb = constr_of_global Coqlib.glob_bool
 
-let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
+let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
 
 let andb_true_intro = fun _ ->
-  Universes.constr_of_global
+  UnivGen.constr_of_global
     (Coqlib.build_bool_type()).Coqlib.andb_true_intro
 
 let tt = constr_of_global Coqlib.glob_true
@@ -76,9 +76,9 @@ let ff = constr_of_global Coqlib.glob_false
 
 let eq = constr_of_global Coqlib.glob_eq
 
-let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ())
+let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ())
 
-let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
+let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
 
 let induct_on c = induction false None c None None
 
@@ -863,7 +863,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
         create_input (
           mkNamedProd n (mkFullInd ind (2*nparrec)) (
             mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
-              mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
+              mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
           )
         )
       )
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 26a46a752..722f21171 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -174,7 +174,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, Universes.constr_of_global_univ (c,u)))
+          (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u)))
           idl refs
       in
       subst'@subst, status' && status, next_uctx uctx)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 32885ab88..2deca1e06 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -380,7 +380,7 @@ let do_mutual_induction_scheme lnamedepindsort =
 	 match inst with
 	 | None ->
 	    let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
-	    let u, ctx = Universes.fresh_instance_from ctx None in
+            let u, ctx = UnivGen.fresh_instance_from ctx None in
             let evd = Evd.from_ctx (UState.of_context_set ctx) in
 	      evd, (ind,u), Some u
 	 | Some ui -> evd, (ind, ui), inst
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6de8539d4..624edeffe 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -259,7 +259,7 @@ let eterm_obligations env name evm fs ?status t ty =
 let tactics_module = ["Program";"Tactics"]
 let safe_init_constant md name () =
   Coqlib.check_required_library ("Coq"::md);
-  Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name)
+  UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name)
 let hide_obligation = safe_init_constant tactics_module "obligation"
 
 let pperror cmd = CErrors.user_err ~hdr:"Program" cmd