From aa5e962c9888889380ae85a7cbd82a8ac4779a0f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 28 Apr 2018 17:26:18 +0200
Subject: Make set minimization option internal to Universes

---
 engine/universes.ml    | 10 +++++++++-
 engine/universes.mli   |  3 ---
 pretyping/pretyping.ml |  8 --------
 3 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/engine/universes.ml b/engine/universes.ml
index a13663cbad..96d49361fd 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -116,7 +116,15 @@ let universe_binders_with_opt_names ref levels = function
 
 let set_minimization = ref true
 let is_set_minimization () = !set_minimization
-			    
+
+let _ =
+  Goptions.(declare_bool_option
+          { optdepr  = false;
+            optname  = "minimization to Set";
+            optkey   = ["Universe";"Minimization";"ToSet"];
+            optread  = is_set_minimization;
+            optwrite = (:=) set_minimization })
+
 type universe_constraint =
   | ULe of Universe.t * Universe.t
   | UEq of Universe.t * Universe.t
diff --git a/engine/universes.mli b/engine/universes.mli
index df2e961d60..46d65f257e 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -17,9 +17,6 @@ open Univ
 (** Unordered pairs of universe levels (ie (u,v) = (v,u)) *)
 module UPairSet : CSet.S with type elt = (Level.t * Level.t)
 
-val set_minimization : bool ref
-val is_set_minimization : unit -> bool
-
 (** Universes *)
 
 val pr_with_global_universes : Level.t -> Pp.t
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 35cc5702a6..62a91c5531 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 =
-- 
cgit v1.2.3