diff options
| author | Matthieu Sozeau | 2014-04-14 17:20:22 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:59:00 +0200 |
| commit | da88175778d6055d1ecf40c8f429cf855a4304cb (patch) | |
| tree | 174c3039927f12b3404d9a5215bc91512200e634 /tactics | |
| parent | 3869ffab2021b076054280f5eb4226ecda8caf75 (diff) | |
Avoid u+k <= v constraints, don't take the sup of an algebraic universe during
minimization.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0fbb511a7d..2db58978d1 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) -> |