Split off Universes functions dealing with generating new universes.

5 files changed, 10 insertions, 10 deletions

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]