diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 2501ce4f26..d63b6dbfce 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -191,12 +191,12 @@ Type@{UnivBinders.57} -> Type@{i} axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axbar -axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i} +axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo' -axbar' : Type@{UnivBinders.59} -> Type@{axbar'.i} +axbar' : Type@{axbar'.u0} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] |