diff options
| author | Matthieu Sozeau | 2015-10-08 16:00:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-08 16:00:41 +0200 |
| commit | b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc (patch) | |
| tree | 1505041402d00c52669f9e430d144c97eae490ff /pretyping/pretyping.ml | |
| parent | dbdef043ea143f871a3710bae36dfc45fd815835 (diff) | |
Univs: fix bug #3807
Add a flag to disallow minimization to set
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index dec23328f4..6306739b7a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -112,6 +112,15 @@ let _ = optkey = ["Strict";"Universe";"Declaration"]; optread = is_strict_universe_declarations; optwrite = (:=) strict_universe_declarations }) + +let _ = + Goptions.(declare_bool_option + { optsync = true; + optdepr = false; + optname = "minimization to Set"; + optkey = ["Universe";"set";"Minimization"]; + optread = Universes.is_set_minimization; + optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) let interp_universe_level_name evd (loc,s) = |