diff options
| author | Gaëtan Gilbert | 2018-10-18 13:04:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-12 18:43:04 +0100 |
| commit | a44b97e3e7f4a302a5255ca9fc57ea0b81a36b7e (patch) | |
| tree | acf701c04456cb7fd91746a7ef4d05fa5544a85b /test-suite | |
| parent | 620bb4184017a8b720f6937f0cba09e93883e812 (diff) | |
Do not qualify universe names by section path.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/unidecls.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v index 1827e54d76..1bc565cbb5 100644 --- a/test-suite/success/unidecls.v +++ b/test-suite/success/unidecls.v @@ -46,12 +46,12 @@ Universe secfoo. Section Foo'. Fail Universe secfoo. Universe secfoo2. - Check Type@{Foo'.secfoo2}. + Fail Check Type@{Foo'.secfoo2}. + Check Type@{secfoo2}. Constraint secfoo2 < a. End Foo'. Check Type@{secfoo2}. -Fail Check Type@{Foo'.secfoo2}. Fail Check eq_refl : Type@{secfoo2} = Type@{a}. (** Below, u and v are global, fixed universes *) |