diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-13 18:42:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-13 22:54:17 +0200 |
| commit | 03a71a241f8d05f6a86f3c8f3c2146c4db378f7b (patch) | |
| tree | 10817571fedddc524e2f3a890f97696a0690e7fd /.gitignore | |
| parent | cbb41129f15623ba5be50026f930e0435c9f5259 (diff) | |
Univs: more robust Universe/Constraint decls #4816
This fixes the declarations of constraints, universes
and assumptions:
- global constraints can refer to global universes only,
- polymorphic universes, constraints and assumptions can only be
declared inside sections, when all the section's
variables/universes are polymorphic as well.
- monomorphic assumptions may only be declared in section contexts
which are not parameterized by polymorphic universes/assumptions.
Add fix for part 1 of bug #4816
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions