diff options
| author | Matthieu Sozeau | 2015-11-27 17:21:35 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-27 17:23:05 +0100 |
| commit | a0e72610a71e086da392c8563c2eec2e35211afa (patch) | |
| tree | 76986613697d29c4970307037a737dbf172f7643 | |
| parent | 8297baa98147f78263126b1bd6cf41b0456f177d (diff) | |
Avoid recording spurious Set <= Top.i constraints which are always
valid (when Top.i is global and hence > Set).
| -rw-r--r-- | library/universes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/universes.ml b/library/universes.ml index 6cccb10efb..1b6f7a9d57 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -854,7 +854,7 @@ 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 - if is_set_minimization () then + if is_set_minimization () && LSet.mem r ctx then (Constraint.add cstr smallles, noneqs) else (smallles, noneqs) else if Level.is_small r then |