Propagate implicit arguments in all notations for partial applications.

This was done for abbreviations but not string notations. This adopts
the policy proposed in #11091 to make parsing and printing consistent.

4 files changed, 33 insertions, 29 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1cfd50e26e..e14629df9b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2070,9 +2070,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             | CRef (ref,us) ->
                intern_applied_reference ~isproj intern env
                  (Environ.named_context_val globalenv) lvar us args ref
-            | CNotation (_,ntn,([],[],[],[])) ->
+            | CNotation (_,ntn,ntnargs) ->
                 assert (Option.is_empty isproj);
-                let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
+                let c = intern_notation intern env ntnvars loc ntn ntnargs in
                 let x, impl, scopes, l = find_appl_head_data c in
                   (x,impl,scopes,l), args
             | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 990a7151b4..9b50b53456 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -226,8 +226,10 @@ where
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
-     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
@@ -240,8 +242,10 @@ where
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
-     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 0b78c388fa..49378ab846 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -299,15 +299,15 @@ Module AppliedTermsPrinting.
   Check ## 0.
   (* ## 0 *)
   Check ## 0 0.
-  (* @p nat 0 0 *)
+  (* ## 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
-  Check ## 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
   Check p 0 0 true.
   (* ## 0 0 true *)
-  Check ## 0 0 bool true.
-  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
+  Check ## 0 0 true.
+  (* ## 0 0 true *)
 
   End NotationForPartialApplication.
 
@@ -325,15 +325,15 @@ Module AppliedTermsPrinting.
   Check ## 0.
   (* ## 0 *)
   Check ## 0 0.
-  (* @p nat 0 0 *)
+  (* ## 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
-  Check ## 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
   Check p 0 0 true.
   (* ## 0 0 true *)
-  Check ## 0 0 bool true.
-  (* ## 0 0 true -- INCONSISTENCY parsing/printing *)
+  Check ## 0 0 true.
+  (* ## 0 0 true *)
 
   End AtNotationForPartialApplication.
 
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index b26e725d9b..986908b7fc 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -7,21 +7,21 @@ The convention is:
 Constant foo with implicit arguments and scopes used in a term or a pattern:
 
        foo      do not deactivate further arguments and scopes
-       @foo     deactivates further arguments and scopes
-       (foo x)  deactivates further arguments and scopes
-       (@foo x) deactivates further arguments and scopes
+       @foo     deactivate further arguments and scopes
+       (foo x)  deactivate further arguments and scopes
+       (@foo x) deactivate further arguments and scopes
 
 Notations binding to foo:
 
 #   := foo      do not deactivate further arguments and scopes
-#   := @foo     deactivates further arguments and scopes
-# x := foo x    deactivates further arguments and scopes
-# x := @foo x   deactivates further arguments and scopes
+#   := @foo     deactivate further arguments and scopes
+# x := foo x    do not deactivate further arguments and scopes
+# x := @foo x   do not deactivate further arguments and scopes
 
 Abbreviations binding to foo:
 
 f   := foo      do not deactivate further arguments and scopes
-f   := @foo     deactivates further arguments and scopes
+f   := @foo     deactivate further arguments and scopes
 f x := foo x    do not deactivate further arguments and scopes
 f x := @foo x   do not deactivate further arguments and scopes
 *)
@@ -62,17 +62,17 @@ Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 
-(* 5. Notations stop further implicit arguments to be inserted and scopes to be used *)
+(* 5. 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 0 0 : prod' bool bool.
-Check # 0 _ 0%bool 0%bool : 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.
 
-(* 6. Notations stop further implicit arguments to be inserted and scopes to be used *)
+(* 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%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.
 
 (* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
@@ -86,9 +86,9 @@ Notation "####" := pair' (at level 0).
 Check #### 0 0 0 : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
 
-(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *)
+(* 9. Non-@id notations inherit implicit arguments and scopes *)
 Notation "##### x" := (pair' x) (at level 0, x at level 1).
-Check ##### 0 _ 0%bool 0%bool : 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.
 
 (* 10. Check computation of binding variable through other notations *)