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 /library | |
| parent | dbdef043ea143f871a3710bae36dfc45fd815835 (diff) | |
Univs: fix bug #3807
Add a flag to disallow minimization to set
Diffstat (limited to 'library')
| -rw-r--r-- | library/universes.ml | 11 | ||||
| -rw-r--r-- | library/universes.mli | 3 |
2 files changed, 13 insertions, 1 deletions
diff --git a/library/universes.ml b/library/universes.ml index bc42cc044c..0656188eb5 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 5527da0903..4ff21d45c9 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 = |