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 | |
| parent | 2cdccb3f050b68fdfa36ab1ac444b7507564cb77 (diff) | |
Fix #10669 incorrect substitution in context outside section
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_10669.v | 12 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.out | 4 |
2 files changed, 14 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_10669.v b/test-suite/bugs/closed/bug_10669.v new file mode 100644 index 0000000000..433e300acb --- /dev/null +++ b/test-suite/bugs/closed/bug_10669.v @@ -0,0 +1,12 @@ + +Context (A0:Type) (B0:A0). +Definition foo0 := B0. + +Set Universe Polymorphism. +Context (A1:Type) (B1:A1). +Definition foo1 := B1. + +Section S. + Context (A2:Type) (B2:A2). + Definition foo2 := B2. +End S. 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] |