diff options
| author | Gaëtan Gilbert | 2018-09-14 13:38:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 4cbbbf0842eab2a996f749957c2e5120d91d6faf (patch) | |
| tree | 15d01d2d21de2ed7a4c19d671b0be3d8d5e0fdd6 | |
| parent | 0d7643dabade293696a377dbc1f858dff2d666f4 (diff) | |
Add test for univ names of polymorphic inductives in sections.
This used to print Var (before #8475, even with explicit binders) but
now doesn't.
| -rw-r--r-- | test-suite/output/UnivBinders.out | 20 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.v | 4 |
2 files changed, 18 insertions, 6 deletions
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 75276c7d0e..01eff57299 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -129,11 +129,19 @@ insec@{v} = Type@{u} -> Type@{v} (* v |= *) insec is universe polymorphic +NonCumulative Inductive insecind@{k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{k} + +For inseccstr: Argument scope is [type_scope] insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic +NonCumulative Inductive insecind@{u k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{u k} + +For inseccstr: Argument scope is [type_scope] inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) @@ -155,24 +163,24 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} -(* i Top.48 Top.49 |= *) +axfoo@{i Top.55 Top.56} : Type@{Top.55} -> Type@{i} +(* i Top.55 Top.56 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} -(* i Top.48 Top.49 |= *) +axbar@{i Top.55 Top.56} : Type@{Top.56} -> Type@{i} +(* i Top.55 Top.56 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axbar -axfoo' : Type@{Top.51} -> Type@{axbar'.i} +axfoo' : Type@{Top.58} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo' -axbar' : Type@{Top.51} -> Type@{axbar'.i} +axbar' : Type@{Top.58} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index f806a9f4f7..9aebce1b9a 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -122,8 +122,12 @@ Section SomeSec. Universe u. Definition insec@{v} := Type@{u} -> Type@{v}. Print insec. + + Inductive insecind@{k} := inseccstr : Type@{k} -> insecind. + Print insecind. End SomeSec. Print insec. +Print insecind. Module SomeMod. Definition inmod@{u} := Type@{u}. |