diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-28 22:28:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | f8e639f3b81ae142f5b529be1ad90210fc259375 (patch) | |
| tree | d73251d05312b34ba8f6e38387c3a07372603588 /vernac/classes.ml | |
| parent | d071eac98b7812ac5c03004b438022900885d874 (diff) | |
Fix interpretation of global universes in univdecl constraints.
Also nicer error when the constraints are impossible.
Diffstat (limited to 'vernac/classes.ml')
0 files changed, 0 insertions, 0 deletions