diff options
| author | herbelin | 2010-10-04 12:03:52 +0000 |
|---|---|---|
| committer | herbelin | 2010-10-04 12:03:52 +0000 |
| commit | e892cdd483eca0c880f338f1e4fd7deecdfc5501 (patch) | |
| tree | 077bcdc3e3a7b7b3f2aa572ba1130ade924de3a0 /test-suite | |
| parent | ee3c7ddaf0ab726594b278d30430123cd60e63fa (diff) | |
Fixing bugs in previous commits about implicit arguments:
- fixing r13483 (supposed dead code in impargs was actually half-living:
implicit arguments mode should merge with the {...} manually given
implicit arguments but not with the "Implicit Arguments [...]" arguments),
- fixing code of drop_first_implicits in r13484.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
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. |