diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-14 17:20:22 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:00 +0200 |
| commit | da88175778d6055d1ecf40c8f429cf855a4304cb (patch) | |
| tree | 174c3039927f12b3404d9a5215bc91512200e634 | |
| parent | 3869ffab2021b076054280f5eb4226ecda8caf75 (diff) | |
Avoid u+k <= v constraints, don't take the sup of an algebraic universe during
minimization.
| -rw-r--r-- | library/universes.ml | 19 | ||||
| -rw-r--r-- | tactics/tactics.ml | 3 |
2 files changed, 13 insertions, 9 deletions
diff --git a/library/universes.ml b/library/universes.ml index b0a610700..6799a99e5 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -463,16 +463,19 @@ exception Stays let compute_lbound left = (** The universe variable was not fixed yet. Compute its level using its lower bound. *) - if CList.is_empty left then None - else - let lbound = List.fold_left (fun lbound (d, l) -> - if d == Le (* l <= ?u *) then (Universe.sup l lbound) + let sup l lbound = + match lbound with + | None -> Some l + | Some l' -> Some (Universe.sup l l') + in + List.fold_left (fun lbound (d, l) -> + if d == Le (* l <= ?u *) then sup l lbound else (* l < ?u *) (assert (d == Lt); - (Universe.sup (Universe.super l) lbound))) - Universe.type0m left - in - Some lbound + if not (Universe.level l == None) then + sup (Universe.super l) lbound + else None)) + None left let maybe_enforce_leq lbound u cstrs = match lbound with diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0fbb511a7..2db58978d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -435,7 +435,8 @@ let id_of_name_with_default id = function let hid = Id.of_string "H" let xid = Id.of_string "X" -let default_id_of_sort = function Prop _ -> hid | Type _ -> xid +let default_id_of_sort s = + if Sorts.is_small s then hid else xid let default_id env sigma = function | (name,None,t) -> |