Made that notations to names behave like the names they refer to wrt

implicit arguments and scope (use Implicit Arguments or Arguments
Scope commands instead if not the desired behaviour).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 7d7bcc71e..316bede93 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -48,3 +48,9 @@ Definition foo P := let '(exists x, Q) := P in x = Q :> nat.
 
 Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat
    (at level 200, x ident, right associativity, y at level 69).
+
+(* Check that notations to atomic references preserve implicit arguments *)
+
+Notation eq := @eq.
+
+Check (eq 0 0).