diff options
| author | Emilio Jesus Gallego Arias | 2020-02-22 15:54:11 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-22 15:54:11 -0500 |
| commit | fe86fb5561f2bbde86236d8c91e973df4393049f (patch) | |
| tree | b593c748432234e0ba990f9e583708fda8a37a71 /test-suite | |
| parent | 53c9fd8339873b2bd77d756a96a2908eb5ce078a (diff) | |
| parent | 2ed097cfba9136a0fba9b961d24c408077fac11d (diff) | |
Merge PR #11596: ComInductive: use lbound=Prop iff non polymorphic
Reviewed-by: ejgallego
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/UnivBinders.out | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 525ca48bee..04514c15cb 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -67,9 +67,9 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.34} in -let ff := Type@{UnivBinders.36} in tt -> ff - : Type@{max(UnivBinders.33,UnivBinders.35)} +let tt := Type@{UnivBinders.33} in +let ff := Type@{UnivBinders.35} in tt -> ff + : Type@{max(UnivBinders.32,UnivBinders.34)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = @@ -142,16 +142,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.59 UnivBinders.60} : -Type@{UnivBinders.59} -> Type@{i} -(* i UnivBinders.59 UnivBinders.60 |= *) +axfoo@{i UnivBinders.58 UnivBinders.59} : +Type@{UnivBinders.58} -> Type@{i} +(* i UnivBinders.58 UnivBinders.59 |= *) axfoo is universe polymorphic Arguments axfoo _%type_scope Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.59 UnivBinders.60} : -Type@{UnivBinders.60} -> Type@{i} -(* i UnivBinders.59 UnivBinders.60 |= *) +axbar@{i UnivBinders.58 UnivBinders.59} : +Type@{UnivBinders.59} -> Type@{i} +(* i UnivBinders.58 UnivBinders.59 |= *) axbar is universe polymorphic Arguments axbar _%type_scope |