diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/polymorphism.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 7eaafc354..00cab744e 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -190,6 +190,8 @@ Module binders. Fail Defined. Abort. + Fail Lemma bar@{u v | } : let x := (fun x => x) : Type@{u} -> Type@{v} in nat. + Lemma bar@{i j| i < j} : Type@{j}. Proof. exact Type@{i}. |