diff options
| author | Matthieu Sozeau | 2016-06-13 18:42:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-13 22:54:17 +0200 |
| commit | 03a71a241f8d05f6a86f3c8f3c2146c4db378f7b (patch) | |
| tree | 10817571fedddc524e2f3a890f97696a0690e7fd /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index efc42aab76..378294c984 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -143,7 +143,7 @@ let interp_universe_level_name evd (loc,s) = with Not_found -> try let id = try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names + evd, snd (Idmap.find id names) with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ~loc ~name:s univ_rigid evd |