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 /library/universes.mli | |
| 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 'library/universes.mli')
| -rw-r--r-- | library/universes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/universes.mli b/library/universes.mli index 53cf5f384..a5740ec49 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -19,7 +19,7 @@ val is_set_minimization : unit -> bool (** Global universe name <-> level mapping *) type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t + (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t val global_universe_names : unit -> universe_names val set_global_universe_names : universe_names -> unit |