diff options
| -rw-r--r-- | pretyping/pretyping.ml | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4519.v | 21 |
2 files changed, 26 insertions, 5 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ac0104d9f..b33084a42 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -138,12 +138,12 @@ let interp_universe_level_name evd (loc,s) = in evd, level else try - let id = - try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names + let level = Evd.universe_of_name evd s in + evd, level with Not_found -> - try let level = Evd.universe_of_name evd s in - evd, level + try + let id = try Id.of_string s with _ -> raise Not_found in + evd, Idmap.find id names with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ~name:s univ_rigid evd diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v new file mode 100644 index 000000000..ccbc47d20 --- /dev/null +++ b/test-suite/bugs/closed/4519.v @@ -0,0 +1,21 @@ +Set Universe Polymorphism. +Section foo. + Universe i. + Context (foo : Type@{i}) (bar : Type@{i}). + Definition qux@{i} (baz : Type@{i}) := foo -> bar. +End foo. +Set Printing Universes. +Print qux. (* qux@{Top.42 Top.43} = +fun foo bar _ : Type@{Top.42} => foo -> bar + : Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} +(* Top.42 Top.43 |= *) +(* This is wrong; the first two types are equal, but the last one is not *) + +qux is universe polymorphic +Argument scopes are [type_scope type_scope type_scope] + *) +Check qux nat nat nat : Set. +Check qux nat nat Set : Set. (* Error: +The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is +expected to have type "Set" +(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
\ No newline at end of file |