Split off Universes functions dealing with generating new universes.

4 files changed, 9 insertions, 9 deletions

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