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 0bd8bfe602..488443de1d 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -159,6 +159,8 @@ End structures. Module binders. + Definition mynat@{|} := nat. + Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}. exact A. Defined. |