Split off Universes functions dealing with generating new universes.

7 files changed, 448 insertions, 311 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]"]