diff options
Diffstat (limited to 'test-suite/success/implicit.v')
| -rw-r--r-- | test-suite/success/implicit.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 59e1a9352..0aa0ae02b 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -86,3 +86,9 @@ Fixpoint plus n m {struct n} := | 0 => m | S p => S (plus p m) end. + +(* Check multiple implicit arguments signatures *) + +Implicit Arguments eq_refl [[A] [x]] [[A]]. + +Check eq_refl : 0 = 0. |