diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/namedunivs.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v index 5c0a3c7f23..059462fac3 100644 --- a/test-suite/success/namedunivs.v +++ b/test-suite/success/namedunivs.v @@ -30,6 +30,9 @@ Definition foo' {A : Type@{i}} (o : option@{i} A) : option@{i} A := Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A := o. + +Definition testm (A : Type@{i}) : Type@{max(i,j)} := A. + (* Inductive prod (A : Type@{i}) (B : Type@{j}) := *) (* | pair : A -> B -> prod A B. *) @@ -43,7 +46,6 @@ Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A := (* | pair _ _ a b => b *) (* end. *) - (* Inductive paths {A : Type} : A -> A -> Type := *) (* | idpath (a : A) : paths a a. *) |