diff options
| author | Pierre-Marie Pédrot | 2019-10-13 16:03:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-13 16:03:43 +0200 |
| commit | 564f265bfda10a2c6d4e7297dec47a14ad4b61b3 (patch) | |
| tree | 17ceaf5d055c0c2a8eb02ccb364d832f5ef694a7 /test-suite | |
| parent | cc4cddda2eb2a05f685c8404e4864ea0bcdac6eb (diff) | |
| parent | 8398ec48072b0bbe5e571a8d1f1f6c1ace9270f4 (diff) | |
Merge PR #10670: ComAssumption cleanup
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
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] |