aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-28 17:26:18 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-17 18:46:09 +0200
commitaa5e962c9888889380ae85a7cbd82a8ac4779a0f (patch)
tree6086365bd58c072e22efb4c5e57133338ed2d991
parent5281317cb558f2b9aa6f854b9c7aeb617beba8e6 (diff)
Make set minimization option internal to Universes
-rw-r--r--engine/universes.ml10
-rw-r--r--engine/universes.mli3
-rw-r--r--pretyping/pretyping.ml8
3 files changed, 9 insertions, 12 deletions
diff --git a/engine/universes.ml b/engine/universes.ml
index a13663cba..96d49361f 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 df2e961d6..46d65f257 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 35cc5702a..62a91c553 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 =