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/output | |
| 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/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] |