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 --- pretyping/pretyping.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'pretyping') 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 = -- cgit v1.2.3