diff options
| -rw-r--r-- | engine/universes.ml | 10 | ||||
| -rw-r--r-- | engine/universes.mli | 3 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 8 |
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 = |