Split off Universes functions dealing with generating new universes.

7 files changed, 19 insertions, 19 deletions

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