diff options
-rw-r--r-- | kernel/univ.ml | 3 | ||||
-rw-r--r-- | kernel/univ.mli | 1 | ||||
-rw-r--r-- | library/universes.ml | 11 | ||||
-rw-r--r-- | library/universes.mli | 3 | ||||
-rw-r--r-- | pretyping/evd.ml | 3 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 9 |
6 files changed, 27 insertions, 3 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 34eb283d7..c0bd3bacd 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1797,6 +1797,9 @@ struct let empty = (LSet.empty, Constraint.empty) let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst + let equal (univs, cst as x) (univs', cst' as y) = + x == y || (LSet.equal univs univs' && Constraint.equal cst cst') + let of_set s = (s, Constraint.empty) let singleton l = of_set (LSet.singleton l) let of_instance i = of_set (Instance.levels i) diff --git a/kernel/univ.mli b/kernel/univ.mli index 4cc8a2528..cbaf7e546 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -360,6 +360,7 @@ sig val of_instance : Instance.t -> t val of_set : universe_set -> t + val equal : t -> t -> bool val union : t -> t -> t val append : t -> t -> t diff --git a/library/universes.ml b/library/universes.ml index bc42cc044..0656188eb 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -26,6 +26,11 @@ let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd !global_universes)) with Not_found -> Level.pr l +(* To disallow minimization to Set *) + +let set_minimization = ref true +let is_set_minimization () = !set_minimization + type universe_constraint_type = ULe | UEq | ULub type universe_constraint = universe * universe_constraint_type * universe @@ -832,7 +837,9 @@ let normalize_context_set ctx us algs = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> if d == Le then if Univ.Level.is_small l then - (Constraint.add cstr smallles, noneqs) + if is_set_minimization () then + (Constraint.add cstr smallles, noneqs) + else (smallles, noneqs) else if Level.is_small r then if Level.is_prop r then raise (Univ.UniverseInconsistency @@ -872,6 +879,8 @@ let normalize_context_set ctx us algs = if d == Eq then (UF.union l r uf; noneqs) else (* We ignore the trivial Prop/Set <= i constraints. *) if d == Le && Univ.Level.is_small l then noneqs + else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r + then noneqs else Constraint.add cstr noneqs) csts Constraint.empty in diff --git a/library/universes.mli b/library/universes.mli index 5527da090..4ff21d45c 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -12,6 +12,9 @@ open Term open Environ open Univ +val set_minimization : bool ref +val is_set_minimization : unit -> bool + (** Universes *) type universe_names = diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 412fb92b3..3d912ca4c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1324,8 +1324,7 @@ let normalize_evar_universe_context uctx = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic in - if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then - uctx + if Univ.ContextSet.equal us' uctx.uctx_local then uctx else let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in let uctx' = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index dec23328f..6306739b7 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) = |