aboutsummaryrefslogtreecommitdiff
path: root/API/API.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2017-09-28 22:28:21 +0200
committerGaëtan Gilbert2017-11-25 14:18:35 +0100
commitf8e639f3b81ae142f5b529be1ad90210fc259375 (patch)
treed73251d05312b34ba8f6e38387c3a07372603588 /API/API.mli
parentd071eac98b7812ac5c03004b438022900885d874 (diff)
Fix interpretation of global universes in univdecl constraints.
Also nicer error when the constraints are impossible.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions