diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/implicit.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 0aa0ae02b0..b142ba7723 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -92,3 +92,10 @@ Fixpoint plus n m {struct n} := Implicit Arguments eq_refl [[A] [x]] [[A]]. Check eq_refl : 0 = 0. + +(* Check that notations preserve implicit (since 8.3) *) + +Parameter p : forall A, A -> forall n, n = 0 -> True. +Implicit Arguments p [A n]. +Notation Q := (p 0). +Check Q eq_refl. |