From 748a33cee41900d285897b24b4d8e29dd9eb2a3d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 28 Apr 2018 21:36:57 +0200
Subject: Split off Universes functions for minimization.

This finishes the splitting of Universes.
---
 engine/universes.mli | 44 +++++++++++++++-----------------------------
 1 file changed, 15 insertions(+), 29 deletions(-)

(limited to 'engine/universes.mli')

diff --git a/engine/universes.mli b/engine/universes.mli
index 4d7105e72..46ff33a47 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -12,37 +12,11 @@ open Names
 open Constr
 open Environ
 open Univ
-open UnivSubst
-
-(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
-module UPairSet : CSet.S with type elt = (Level.t * Level.t)
-
-(** Universes *)
-
-(** Simplification and pruning of constraints:
-    [normalize_context_set ctx us]
-
-    - Instantiate the variables in [us] with their most precise
-    universe levels respecting the constraints.
-
-    - Normalizes the context [ctx] w.r.t. equality constraints, 
-    choosing a canonical universe in each equivalence class 
-    (a global one if there is one) and transitively saturate
-    the constraints w.r.t to the equalities. *)
-
-val normalize_context_set : UGraph.t -> ContextSet.t ->
-  universe_opt_subst (* The defined and undefined variables *) ->
-  LSet.t (* univ variables that can be substituted by algebraics *) ->
-  UPairSet.t (* weak equality constraints *) ->
-  (universe_opt_subst * LSet.t) in_universe_context_set
-
-(** *********************************** Deprecated *)
 
+(** ************************************** *)
+(** This entire module is deprecated. **** *)
+(** ************************************** *)
 [@@@ocaml.warning "-3"]
-val set_minimization : bool ref
-[@@ocaml.deprecated "Becoming internal."]
-val is_set_minimization : unit -> bool
-[@@ocaml.deprecated "Becoming internal."]
 
 (** ****** Deprecated: moved to [UnivNames] *)
 
@@ -250,3 +224,15 @@ 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
 [@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"]
+
+(** ****** Deprecated: moved to [UnivMinim] *)
+
+module UPairSet = UnivMinim.UPairSet
+[@@ocaml.deprecated "Use [UnivMinim.UPairSet]"]
+
+val normalize_context_set : UGraph.t -> ContextSet.t ->
+  universe_opt_subst (* The defined and undefined variables *) ->
+  LSet.t (* univ variables that can be substituted by algebraics *) ->
+  UPairSet.t (* weak equality constraints *) ->
+  (universe_opt_subst * LSet.t) in_universe_context_set
+[@@ocaml.deprecated "Use [UnivMinim.normalize_context_set]"]
-- 
cgit v1.2.3