diff options
| author | Gaëtan Gilbert | 2019-08-19 16:46:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-05 12:10:24 +0200 |
| commit | d7f11221f797e501fe3bcdb06fe7ef3f559869c3 (patch) | |
| tree | 3e98ac43fcac7740d31cff171e56bc499309164e /test-suite/output | |
| parent | 2cdccb3f050b68fdfa36ab1ac444b7507564cb77 (diff) | |
Fix #10669 incorrect substitution in context outside section
Diffstat (limited to 'test-suite/output')
| -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 a89fd64999..d13ea707bb 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -157,12 +157,12 @@ Type@{UnivBinders.58} -> Type@{i} axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axbar -axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i} +axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo' -axbar' : Type@{axbar'.u0} -> Type@{axbar'.i} +axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axbar' is not universe polymorphic Argument scope is [type_scope] |