Inherit scopes and implicit sign. in notations for partially applied pattern.

Exception: when the notation is to some @id.

Formerly, this was ignored for all kinds of string notations.

1 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index dca0208fb0..f166a53256 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -66,14 +66,14 @@ Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2
 Notation "# x" := (pair' x) (at level 0, x at level 1).
 Check pair' 0 0 0 : prod' bool bool.
 Check # 0 0 0 : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with # 0 y 0 => 2 | _ => 1 end.
 
 (* 6. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *)
 Notation "## x" := ((@pair') _ x) (at level 0, x at level 1).
 Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool.
 Check ## 0%bool 0 0 : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with ## 0%bool y 0 => 2 | _ => 1 end.
 
 (* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
 Notation "###" := (@pair') (at level 0).
@@ -89,7 +89,7 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
 (* 9. Non-@id notations inherit implicit arguments and scopes *)
 Notation "##### x" := (pair' x) (at level 0, x at level 1).
 Check ##### 0 0 0 : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with ##### 0 y 0 => 2 | _ => 1 end.
 
 (* 10. Check computation of binding variable through other notations *)
 (* it should be detected as binding variable and the scopes not being checked *)