Merge PR #7384: Split Universes

8 files changed, 23 insertions, 33 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index afa8a12fc0..7dbef01c22 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 49c429458a..062136ff52 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 3327c250d7..40f4d4ff89 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/pretyping.ml b/pretyping/pretyping.ml
index 616ccf0cfb..6bf852fcd9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -169,14 +169,6 @@ let _ =
 	    optread  = is_strict_universe_declarations;
 	    optwrite = (:=) strict_universe_declarations })
 
-let _ =
-  Goptions.(declare_bool_option
-	  { optdepr  = false;
-	    optname  = "minimization to Set";
-	    optkey   = ["Universe";"Minimization";"ToSet"];
-	    optread  = Universes.is_set_minimization;
-	    optwrite = (:=) Universes.set_minimization })
-
 (** Miscellaneous interpretation functions *)
 
 let interp_known_universe_level evd r =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a4d4479026..34d7a07984 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))
 
 
@@ -701,18 +701,18 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
 let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Anonymous -> bd
   | Name.Name id ->
-    let open Universes in
+    let open UnivProblem in
     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 ->
         let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
         begin match csts with
         | Some csts ->
-          let subst = Constraints.fold (fun cst acc ->
+          let subst = Set.fold (fun cst acc ->
               let l, r = match cst with
                 | ULub (u, v) | UWeak (u, v) -> u, v
                 | UEq (u, v) | ULe (u, v) ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4386144fe2..11cc6c1f00 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/pretyping/unification.ml b/pretyping/unification.ml
index 1caa629ffb..62bee5a362 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -561,16 +561,16 @@ let is_rigid_head sigma flags t =
     | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
 
 let force_eqs c =
-  let open Universes in
-  Constraints.fold
+  let open UnivProblem in
+  Set.fold
     (fun c acc ->
        let c' = match c with
          (* Should we be forcing weak constraints? *)
          | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r)
          | ULe _ | UEq _ -> c
        in
-        Constraints.add c' acc)
-    c Constraints.empty
+        Set.add c' acc)
+    c Set.empty
 
 let constr_cmp pb env sigma flags t u =
   let cstrs =
@@ -1504,8 +1504,7 @@ let indirectly_dependent sigma c d decls =
 
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
-  let sigma, subst = nf_univ_variables sigma in
-  (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
+  (sigma, nf_evar sigma c)
 
 let default_matching_core_flags sigma =
   let ts = Names.full_transparent_state in {
@@ -1593,9 +1592,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   (fun test -> match test.testing_state with
   | None -> None
   | Some (sigma,_,l) ->
-     let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in
-     let univs, subst = nf_univ_variables sigma in
-     Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
+     let c = applist (local_strong whd_meta sigma c, l) in
+     Some (sigma, c))
 
 let make_eq_test env evd c =
   let out cstr =
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index e15c3ad042..304a5dadd5 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -32,8 +32,8 @@ type goal_reference =
   | NthGoal of int
   | GoalId of Id.t
 
-type univ_name_list = Universes.univ_name_list
-[@@ocaml.deprecated "Use [Universes.univ_name_list]"]
+type univ_name_list = UnivNames.univ_name_list
+[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
 
 type printable =
   | PrintTables
@@ -49,7 +49,7 @@ type printable =
   | PrintMLLoadPath
   | PrintMLModules
   | PrintDebugGC
-  | PrintName of reference or_by_notation * Universes.univ_name_list option
+  | PrintName of reference or_by_notation * UnivNames.univ_name_list option
   | PrintGraph
   | PrintClasses
   | PrintTypeClasses
@@ -65,7 +65,7 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * Universes.univ_name_list option * Goal_select.t option
+  | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
   | PrintStrategy of reference or_by_notation option