From d6467c2fea8a29634ca649850784c95ed5b9d4f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Nov 2019 13:17:12 +0100
Subject: Fixing anomaly from #11091 (incompatible printing with notation and
 imp. args).

We fix also an index error in deciding when to explicit print a
non-inferable implicit argument.
---
 interp/constrextern.ml           |  6 ++++--
 test-suite/output/Notations5.out | 20 ++++++++++++--------
 test-suite/output/Notations5.v   | 24 ++++++++++++------------
 3 files changed, 28 insertions(+), 22 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 38dc10a9b3..82ba559406 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -742,7 +742,7 @@ let extern_applied_ref inctx impl (cf,f) us args =
 let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs =
   try
     let syndefargs = List.map (fun a -> (a,None)) syndefargs in
-    let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in
+    let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in
     let args = syndefargs @ extraargs in
     if args = [] then cf else CApp ((None, CAst.make cf), args)
   with Expl ->
@@ -762,8 +762,10 @@ let extern_applied_notation n impl f args =
   if List.is_empty args then
     f.CAst.v
   else
-    let args = adjust_implicit_arguments false (List.length args) 1 args impl in
+  try
+    let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in
     mkFlattenedCApp (f,args)
+  with Expl -> raise No_match
 
 let extern_args extern env args =
   let map (arg, argscopes) = lazy (extern argscopes env arg) in
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index c5b4d6f291..96687ed07f 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -138,7 +138,7 @@ v 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-v 0 (B:=bool) true
+v 0 true
      : 0 = 0 /\ true = true
 v
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@@ -158,7 +158,7 @@ v 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-v 0 (B:=bool) true
+v 0 true
      : 0 = 0 /\ true = true
 v
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@@ -188,9 +188,9 @@ where
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
@@ -226,23 +226,27 @@ p 0 0 true
      : 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 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
 ## 0
      : 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 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
-## 0 0 (B:=bool) true
+## 0 0 true
      : 0 = 0 /\ true = true
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index b3bea929ba..3c25547aac 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -181,7 +181,7 @@ Module AppliedTermsPrinting.
   Check v 0.
   (* v 0 *)
   Check v 0 true.
-  (* v 0 (B:=bool) true -- BUG *)
+  (* v 0 true *)
   Check @p nat 0.
   (* v *)
   Check @p nat 0 0.
@@ -209,7 +209,7 @@ Module AppliedTermsPrinting.
   Check v 0.
   (* v 0 *)
   Check v 0 true.
-  (* v 0 (B:=bool) true -- BUG *)
+  (* v 0 true *)
   Check @p nat 0.
   (* v *)
   Check @p nat 0 0.
@@ -243,9 +243,9 @@ Module AppliedTermsPrinting.
   Check ## 0 0.
   (* ## 0 0 *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check ## 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
   Check ## 0 0 (B:=bool).
@@ -298,16 +298,16 @@ Module AppliedTermsPrinting.
   (* ## 0 *)
   Check ## 0.
   (* ## 0 *)
-  (* Check ## 0 0. *)
-  (* Anomaly *)
+  Check ## 0 0.
+  (* @p nat 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
   Check ## 0 0 bool.
   (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check ## 0 0 bool true.
-  (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *)
+  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
 
   End NotationForPartialApplication.
 
@@ -324,16 +324,16 @@ Module AppliedTermsPrinting.
   (* ## 0 *)
   Check ## 0.
   (* ## 0 *)
-  (* Check ## 0 0. *)
-  (* Anomaly *)
+  Check ## 0 0.
+  (* @p nat 0 0 *)
   Check p 0 0 (B:=bool).
   (* ## 0 0 (B:=bool) *)
   Check ## 0 0 bool.
   (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
   Check p 0 0 true.
-  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  (* ## 0 0 true *)
   Check ## 0 0 bool true.
-  (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *)
+  (* ## 0 0 true -- INCONSISTENCY parsing/printing *)
 
   End AtNotationForPartialApplication.
 
-- 
cgit v1.2.3


From 50a39015ea0c86cdb6d368ff7f92ce2091085146 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:19:27 +0100
Subject: Fixing a notation printing bug (missing a @ to reflect absence of
 imp. args).

When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
---
 interp/constrextern.ml           | 3 +--
 test-suite/output/Notations5.out | 4 ++--
 test-suite/output/Notations5.v   | 4 ++--
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 82ba559406..5098b2a00c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1216,7 +1216,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
               (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
               (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
               args2, args2scopes, args2impls
-          | None when nallargs > 0 ->
+          | None ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
@@ -1226,7 +1226,6 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
             | _ -> t, [], [], []
             end
-          | None -> t, [], [], []
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 96687ed07f..7afb5ad396 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -104,9 +104,9 @@ u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 3c25547aac..92ac4b03ff 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -145,9 +145,9 @@ Module AppliedTermsPrinting.
   Check p.
   (* u *)
   Check @p.
-  (* u -- BUG *)
+  (* @u *)
   Check @u.
-  (* u -- BUG *)
+  (* @u *)
   Check u.
   (* u *)
   Check p 0 0.
-- 
cgit v1.2.3


From 67e16fdeef26455d0afa357e31de8f7b3f772034 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:30:05 +0100
Subject: Fixing printing of notations bound to an expression of the form "@f".

The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[])
encoding of @f was lost.

It remains to let printing match parsing wrt the deactivation of
implicit arguments and argument scopes in such case. See next commit.
---
 interp/constrextern.ml           | 10 ++--------
 test-suite/output/Notations5.out | 30 +++++++++++++++---------------
 test-suite/output/Notations5.v   | 30 +++++++++++++++---------------
 3 files changed, 32 insertions(+), 38 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5098b2a00c..681d6ba541 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1209,23 +1209,17 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             [], [] in
         (* Adjust to the number of arguments expected by the notation *)
         let (t,args,argsscopes,argsimpls) = match n with
-          | Some n when nallargs >= n && nallargs > 0 ->
+          | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
               let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
               let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
               (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
-              (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
-              args2, args2scopes, args2impls
+              DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
           | None ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
             end
-          | Some 0 when nallargs = 0 ->
-            begin match DAst.get f with
-            | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
-            | _ -> t, [], [], []
-            end
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 7afb5ad396..9287ea1d4f 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -78,27 +78,27 @@ f
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
 f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-p
+u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-p
+u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0 0
+u 0 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+u 0 0
      : forall b : bool, 0 = 0 /\ b = b
-@p nat 0 0
+@u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-@p nat 0 0
+@u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
@@ -196,7 +196,7 @@ where
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-p
+##
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -204,23 +204,23 @@ where
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 ##
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0
+## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-p 0
+## 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
-p 0 0
+## 0 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+## 0 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+## 0 0
      : forall b : bool, 0 = 0 /\ b = b
-p 0 0 true
+## 0 0 true
      : 0 = 0 /\ true = true
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 92ac4b03ff..81cedc03b4 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -115,21 +115,21 @@ Module AppliedTermsPrinting.
   Notation u := @p.
 
   Check u _.
-  (* p *)
+  (* u -- INCONSISTENT parsing/printing *)
   Check p.
-  (* p *)
-  Check @p.
   (* u *)
+  Check @p.
+  (* @u -- INCONSISTENT parsing/printing *)
   Check u.
-  (* u *)
+  (* @u -- INCONSISTENT parsing/printing *)
   Check p 0 0.
-  (* p 0 0 *)
+  (* u 0 0 *)
   Check u nat 0 0 bool.
-  (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *)
+  (* u 0 0 -- INCONSISTENT parsing/printing *)
   Check u nat 0 0.
-  (* @p nat 0 0 *)
+  (* @u nat 0 0 *)
   Check @p nat 0 0.
-  (* @p nat 0 0 *)
+  (* @u nat 0 0 *)
 
   End AtAbbreviationForApplicationHead.
 
@@ -263,25 +263,25 @@ Module AppliedTermsPrinting.
   Notation "##" := @p (at level 0).
 
   Check p.
-  (* p *)
+  (* ## -- INCONSISTENT parsing/printing *)
   Check @p.
   (* ## *)
   Check ##.
   (* ## *)
   Check p 0.
-  (* p 0 -- why not "## nat 0" *)
+  (* ## 0 *)
   Check ## nat 0.
-  (* p 0 *)
+  (* ## 0 -- INCONSISTENT parsing/printing *)
   Check ## nat 0 0.
   (* @p nat 0 0 *)
   Check p 0 0.
-  (* p 0 0 *)
+  (* ## 0 0 *)
   Check ## nat 0 0 _.
-  (* p 0 0 *)
+  (* ## 0 0 -- INCONSISTENT parsing/printing *)
   Check ## nat 0 0 bool.
-  (* p 0 0 (B:=bool) *)
+  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
   Check ## nat 0 0 bool true.
-  (* p 0 0 true *)
+  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
 
   End AtNotationForHeadApplication.
 
-- 
cgit v1.2.3


From 556e9dde62b6822db20bd5c7e6e6a67bc717c408 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:31:37 +0100
Subject: Deactivate implicit arguments in printing notations bound to "@f".

This is to match the parsing policy (see #11091).

In particular, we deactivate also argument scopes, consistently with
what is done at parsing time.
---
 interp/constrextern.ml           | 11 ++++++++---
 test-suite/output/Notations.out  |  9 +++++----
 test-suite/output/Notations5.out | 32 ++++++++++++++++----------------
 test-suite/output/Notations5.v   | 32 ++++++++++++++++----------------
 4 files changed, 45 insertions(+), 39 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 681d6ba541..362fe83ffa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1211,9 +1211,14 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
         let (t,args,argsscopes,argsimpls) = match n with
           | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
-              let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
-              let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
-              (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
+              let args2scopes =
+                if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in
+              let args2impls =
+                if n = 0 then
+                  (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
+                     conventionally deactivates implicit arguments *)
+                  []
+                else try List.skipn n argsimpls with Failure _ -> [] in
               DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
           | None ->
             begin match DAst.get f with
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b870fa6f6f..2966c1126d 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,10 +111,11 @@ fun x : option Z => match x with
                     | NONE2 => 0
                     end
      : option Z -> Z
-fun x : list ?T => match x with
-                   | NIL => NONE2
-                   | (_ :') t => SOME2 t
-                   end
+fun x : list ?T =>
+match x with
+| NIL => NONE3 (list ?T)
+| (_ :') t => SOME3 (list ?T) t
+end
      : list ?T -> option (list ?T)
 where
 ?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 9287ea1d4f..990a7151b4 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -78,27 +78,27 @@ f
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
 f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-u
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-@u
+u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-@u
+u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u 0 0
+u nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-u 0 0
+u nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-@u nat 0 0
+u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-@u nat 0 0
+u nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
@@ -196,7 +196,7 @@ where
      : forall b : bool, 0 = 0 /\ b = b
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-##
+## ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -204,23 +204,23 @@ where
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 ##
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-## 0
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-## 0
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-@p nat 0 0
+## nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
-## 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-## 0 0
+## nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-## 0 0 true
+## nat 0 0 bool true
      : 0 = 0 /\ true = true
 ## 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 81cedc03b4..0b78c388fa 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -115,21 +115,21 @@ Module AppliedTermsPrinting.
   Notation u := @p.
 
   Check u _.
-  (* u -- INCONSISTENT parsing/printing *)
+  (* u ?A *)
   Check p.
-  (* u *)
+  (* u ?A *)
   Check @p.
-  (* @u -- INCONSISTENT parsing/printing *)
+  (* u *)
   Check u.
-  (* @u -- INCONSISTENT parsing/printing *)
+  (* u *)
   Check p 0 0.
-  (* u 0 0 *)
+  (* u nat 0 0 ?B *)
   Check u nat 0 0 bool.
-  (* u 0 0 -- INCONSISTENT parsing/printing *)
+  (* u nat 0 0 bool *)
   Check u nat 0 0.
-  (* @u nat 0 0 *)
+  (* u nat 0 0 *)
   Check @p nat 0 0.
-  (* @u nat 0 0 *)
+  (* u nat 0 0 *)
 
   End AtAbbreviationForApplicationHead.
 
@@ -263,25 +263,25 @@ Module AppliedTermsPrinting.
   Notation "##" := @p (at level 0).
 
   Check p.
-  (* ## -- INCONSISTENT parsing/printing *)
+  (* ## ?A *)
   Check @p.
   (* ## *)
   Check ##.
   (* ## *)
   Check p 0.
-  (* ## 0 *)
+  (* ## nat 0 *)
   Check ## nat 0.
-  (* ## 0 -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 *)
   Check ## nat 0 0.
-  (* @p nat 0 0 *)
+  (* ## nat 0 0 *)
   Check p 0 0.
-  (* ## 0 0 *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 _.
-  (* ## 0 0 -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 bool.
-  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 bool *)
   Check ## nat 0 0 bool true.
-  (* ## 0 0 true -- INCONSISTENT parsing/printing *)
+  (* ## nat 0 0 bool true *)
 
   End AtNotationForHeadApplication.
 
-- 
cgit v1.2.3


From 14196d8ab425f67faf3995bd29a003de3b2e87ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 08:26:14 +0100
Subject: 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.
---
 interp/constrintern.ml           |  4 ++--
 test-suite/output/Notations5.out | 12 ++++++++----
 test-suite/output/Notations5.v   | 20 ++++++++++----------
 test-suite/success/Notations2.v  | 26 +++++++++++++-------------
 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 *)
-- 
cgit v1.2.3


From 04b9870f0ebe79fde789551c8e172aad1e7cfc5c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 08:52:01 +0100
Subject: Inherit argument scopes in notations to expressions of the form @f.

This is a change of semantics.
---
 interp/constrextern.ml          | 3 +--
 interp/constrintern.ml          | 4 ++--
 test-suite/success/Notations2.v | 9 +++++++++
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 362fe83ffa..7f5f03610b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1211,8 +1211,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
         let (t,args,argsscopes,argsimpls) = match n with
           | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
-              let args2scopes =
-                if n = 0 then [] else try List.skipn n argsscopes with Failure _ -> [] in
+              let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
               let args2impls =
                 if n = 0 then
                   (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e14629df9b..1149cf1f58 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1071,11 +1071,11 @@ let find_appl_head_data c =
       c, impls, scopes, []
   | GApp (r, l) ->
     begin match DAst.get r with
-    | GRef (ref,_) when l != [] ->
+    | GRef (ref,_) ->
       let n = List.length l in
       let impls = implicits_of_global ref in
       let scopes = find_arguments_scope ref in
-        c, List.map (drop_first_implicits n) impls,
+        c, (if n = 0 then [] else List.map (drop_first_implicits n) impls),
         List.skipn_at_least n scopes,[]
     | _ -> c,[],[],[]
     end
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 986908b7fc..dca0208fb0 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -185,3 +185,12 @@ Import A.
 Infix "+++" := Nat.add (at level 80).
 
 End M18.
+
+Module InheritanceArgumentScopes.
+
+Axiom p : forall (A:Type) (b:nat), A = A /\ b = b.
+Check fun A n => p (A * A) (n * n). (* safety check *)
+Notation q := @p.
+Check fun A n => q (A * A) (n * n). (* check that argument scopes are propagated *)
+
+End InheritanceArgumentScopes.
-- 
cgit v1.2.3


From ba52fd0dff4dcf06621fb91ff4902a060a0b222d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 11:36:51 +0100
Subject: Use auxiliary function for externing record patterns.

Also apply the same conditions for printing constructors as record
instances in both terms and patterns.
---
 interp/constrextern.ml     | 54 ++++++++++++++++++++++++++++------------------
 test-suite/output/Record.v |  2 ++
 2 files changed, 35 insertions(+), 21 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7f5f03610b..c68a60fc93 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -403,6 +403,36 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
       (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
   ) impl_st
 
+let extern_record_pattern cstrsp args =
+  try
+    if !Flags.raw_print then raise Exit;
+    let projs = Recordops.lookup_projections (fst cstrsp) in
+    if PrintingRecord.active (fst cstrsp) then
+      ()
+    else if PrintingConstructor.active (fst cstrsp) then
+      raise Exit
+    else if not (get_record_print ()) then
+      raise Exit;
+    let rec ip projs args acc =
+      match projs, args with
+      | [], [] -> acc
+      | proj :: q, pat :: tail ->
+        let acc =
+          match proj, pat with
+          | _, { CAst.v = CPatAtom None } ->
+            (* we don't want to have 'x := _' in our patterns *)
+            acc
+          | Some c, _ ->
+            let loc = pat.CAst.loc in
+            (extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc
+          | _ -> raise No_match in
+        ip q tail acc
+      | _ -> assert false
+    in
+    Some (List.rev (ip projs args []))
+  with
+    Not_found | No_match | Exit -> None
+
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
@@ -437,27 +467,9 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
         | PatCstr(cstrsp,args,na) ->
           let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
           let p =
-            try
-              if !Flags.raw_print then raise Exit;
-              let projs = Recordops.lookup_projections (fst cstrsp) in
-              let rec ip projs args acc =
-                match projs, args with
-                  | [], [] -> acc
-                  | proj :: q, pat :: tail ->
-                     let acc =
-                       match proj, pat with
-                       | _, { CAst.v = CPatAtom None } ->
-                          (* we don't want to have 'x := _' in our patterns *)
-                          acc
-                       | Some c, _ ->
-                          ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
-                       | _ -> raise No_match in
-                     ip q tail acc
-                  | _ -> assert false
-              in
-              CPatRecord(List.rev (ip projs args []))
-            with
-                Not_found | No_match | Exit ->
+            match extern_record_pattern cstrsp args with
+            | Some l -> CPatRecord l
+            | None ->
                   let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
                   if Constrintern.get_asymmetric_patterns () then
                     if pattern_printable_in_both_syntax cstrsp
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index d9a649fadc..71a8afa131 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,6 +20,8 @@ Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
 
+Set Printing Records.
+
 Record N := C { T : Type; _ : True }.
 Check fun x:N => let 'C _ p := x in p.
 Check fun x:N => let 'C T _ := x in T.
-- 
cgit v1.2.3


From 3eea1e383e23ea76fcd49a7b302f31b2e3f6ef2a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 12:14:37 +0100
Subject: Fix inheritance of argument scopes when printing notations in
 patterns.

---
 interp/constrextern.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c68a60fc93..008e84cd9c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -508,7 +508,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
                 let subscope = (subentry,(scopt,scl@scopes')) in
                 List.map (extern_cases_pattern_in_scope subscope vars) c)
                 substlist in
-            let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+            let subscopes = find_arguments_scope gr in
+            let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
+            let more_args = fill_arg_scopes more_args more_args_scopes allscopes in
+            let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
             let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
               else
                 match drop_implicits_in_patt gr nb_to_drop l2 with
@@ -528,7 +531,10 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
         List.rev_map (fun (c,(subentry,(scopt,scl))) ->
           extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
           subst in
-      let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+      let subscopes = find_arguments_scope gr in
+      let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
+      let more_args = fill_arg_scopes more_args more_args_scopes allscopes in
+      let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
         else
           match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
-- 
cgit v1.2.3


From 32467acf285629c28cbda27d27a8cf248150f2bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 12:44:44 +0100
Subject: Fix index bug in computing implicit signature of abbrev. in pattern
 printing.

---
 interp/constrextern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 008e84cd9c..b05ca8e5a6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -537,7 +537,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
       let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
         else
-          match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
+          match drop_implicits_in_patt gr nb_to_drop l2 with
             |Some true_args -> true_args
             |None -> raise No_match
       in
-- 
cgit v1.2.3


From 8d80875d230bd8af5611ec04bced1e5a17d058b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 12:46:42 +0100
Subject: 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.
---
 interp/constrintern.ml          | 12 ++++++++++--
 test-suite/success/Notations2.v |  6 +++---
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1149cf1f58..1b9b45c3fb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1680,7 +1680,7 @@ let drop_notations_pattern looked_for genv =
           test_kind top g;
           Dumpglob.add_glob ?loc:qid.loc g;
           let (_,argscs) = find_remaining_scopes [] pats g in
-          Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
+          Some (g,[],List.map2 (in_pat_sc scopes) argscs pats)
     with Not_found -> None
   and in_pat top scopes pt =
     let open CAst in
@@ -1780,7 +1780,15 @@ let drop_notations_pattern looked_for genv =
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
       let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
       let pl = add_local_defs_and_check_length loc genv g pl args in
-      DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
+      let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in
+      let pat =
+        if List.length pl = 0 then
+          (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then
+             implicit arguments are not inherited *)
+          RCPatCstr (g, pl @ args, [])
+        else
+          RCPatCstr (g, pl, args) in
+      DAst.make ?loc @@ pat
     | NList (x,y,iter,terminator,revert) ->
       if not (List.is_empty args) then user_err ?loc
         (strbrk "Application of arguments to a recursive notation not supported in patterns.");
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 *)
-- 
cgit v1.2.3


From 9da7715108554a5105c012685e90b2fa563abf08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 13:41:00 +0100
Subject: In printing patterns, distinguish the case of a notation to @id.

This is a case which conventionally deactivates implicit arguments.
---
 interp/constrextern.ml          |  8 +++++---
 interp/notation_ops.ml          | 21 ++++++++++++---------
 interp/notation_ops.mli         |  4 ++--
 test-suite/output/Notations.out |  4 ++--
 4 files changed, 21 insertions(+), 16 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b05ca8e5a6..4ec9f17c71 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -485,7 +485,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
       in
       insert_pat_coercion coercion pat
 
-and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
+and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop,more_args))
     (custom, (tmp_scope, scopes) as allscopes) vars =
   function
     | NotationRule (_,ntn as specific_ntn) ->
@@ -514,7 +514,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
             let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
             let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
               else
-                match drop_implicits_in_patt gr nb_to_drop l2 with
+                if no_implicit then l2 else
+                  match drop_implicits_in_patt gr nb_to_drop l2 with
                   |Some true_args -> true_args
                   |None -> raise No_match
             in
@@ -537,7 +538,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
       let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
         else
-          match drop_implicits_in_patt gr nb_to_drop l2 with
+          if no_implicit then l2 else
+            match drop_implicits_in_patt gr nb_to_drop l2 with
             |Some true_args -> true_args
             |None -> raise No_match
       in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d1eb50d370..59a58d643c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1364,35 +1364,37 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert =
 
 let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
-  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
-  | PatVar Anonymous, NHole _ -> sigma,(0,[])
+  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
+  | PatVar Anonymous, NHole _ -> sigma,(false,0,[])
   | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
       let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
-      sigma,(0,l)
+      sigma,(false,0,l)
   | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
       let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
-      if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
+      if le2 > List.length l1
       then
         raise No_match
       else
         let l1',more_args = Util.List.chop le2 l1 in
-        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        (* Convention: notations to @f don't keep implicit arguments *)
+        let no_implicit = le2 = 0 in
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
   | r1, NList (x,y,iter,termin,revert) ->
       (match_cases_pattern_list (match_cases_pattern_no_more_args)
-        metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[])
+        metas (terms,termlists,(),()) a1 x y iter termin revert),(false,0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
     match match_cases_pattern metas sigma a1 a2 with
-      | out,(_,[]) -> out
+      | out,(_,_,[]) -> out
       | _ -> raise No_match
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
   | NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
-      sigma,(0,pats)
+      sigma,(false,0,pats)
   | NApp (NRef (GlobRef.IndRef r2),l2)
       when eq_ind ind r2 ->
       let le2 = List.length l2 in
@@ -1401,7 +1403,8 @@ let match_ind_pattern metas sigma ind pats a2 =
         raise No_match
       else
         let l1',more_args = Util.List.chop le2 pats in
-        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        let no_implicit = le2 = 0 in
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
   |_ -> raise No_match
 
 let reorder_canonically_substitution terms termlists metas =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c62dac013b..2ab8b620df 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -69,12 +69,12 @@ val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
 val match_notation_constr_cases_pattern :
   'a cases_pattern_g -> interpretation ->
   (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
-    (int * 'a cases_pattern_g list)
+    (bool * int * 'a cases_pattern_g list)
 
 val match_notation_constr_ind_pattern :
   inductive -> 'a cases_pattern_g list -> interpretation ->
   (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
-    (int * 'a cases_pattern_g list)
+    (bool * int * 'a cases_pattern_g list)
 
 (** {5 Matching a notation pattern against a [glob_constr]} *)
 
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 2966c1126d..53ad8a9612 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -107,8 +107,8 @@ fun x : option Z => match x with
                     end
      : option Z -> Z
 fun x : option Z => match x with
-                    | SOME2 x0 => x0
-                    | NONE2 => 0
+                    | SOME3 _ x0 => x0
+                    | NONE3 _ => 0
                     end
      : option Z -> Z
 fun x : list ?T =>
-- 
cgit v1.2.3


From a905e70df85ef7bf700bb3d6a1b48ae180dfa987 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 13:42:35 +0100
Subject: Inherit arguments scopes in pattern notations bound to some @id.

---
 interp/constrintern.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1b9b45c3fb..f68f4e67b9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1659,10 +1659,11 @@ let drop_notations_pattern looked_for genv =
           let () = assert (List.is_empty vars) in
           let (_,argscs) = find_remaining_scopes [] pats g in
           Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
-        | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
+        | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
               test_kind top g;
               let () = assert (List.is_empty vars) in
-              Some (g, List.map (in_pat false scopes) pats, [])
+              let (_,argscs) = find_remaining_scopes [] pats g in
+              Some (g, List.map2 (in_pat_sc scopes) argscs pats, [])
         | NApp (NRef g,args) ->
               (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
               test_kind top g;
-- 
cgit v1.2.3


From 02cdbd221183b985460dedd49d74b07f4b647bcd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 14:24:32 +0100
Subject: New parsing/printing pattern/terms imp/scopes tests summarizing last
 changes.

---
 test-suite/output/Notations5.out | 56 ++++++++++++++++++++++++++++++++++++++
 test-suite/output/Notations5.v   | 58 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 114 insertions(+)

diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 9b50b53456..f59306c454 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -254,3 +254,59 @@ where
      : 0 = 0 /\ true = true
 ## 0 0 true
      : 0 = 0 /\ true = true
+# 0 0 bool 0%bool
+     : T
+fun a : T => match a with
+             | # 0 0 _ _ => 1
+             | _ => 2
+             end
+     : T -> nat
+#' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | #' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+## 0 0 0%bool
+     : T
+fun a : T => match a with
+             | ## 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+##' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | ##' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+P 0 0 bool 0%bool
+     : T
+fun a : T => match a with
+             | P 0 0 _ _ => 1
+             | _ => 2
+             end
+     : T -> nat
+P' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | P' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+Q 0 0 0%bool
+     : T
+fun a : T => match a with
+             | Q 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
+Q' 0 0 0%bool
+     : T
+fun a : T => match a with
+             | Q' 0 0 _ => 1
+             | _ => 2
+             end
+     : T -> nat
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 49378ab846..09d5e31c48 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -338,3 +338,61 @@ Module AppliedTermsPrinting.
   End AtNotationForPartialApplication.
 
 End AppliedTermsPrinting.
+
+Module AppliedPatternsPrinting.
+
+  (* Other tests testing inheritance of scope and implicit in
+     term and pattern for parsing and printing *)
+
+  Inductive T := p (a:nat) (b:bool) {B} (b:B) : T.
+  Notation "0" := true : bool_scope.
+
+  Module A.
+  Notation "#" := @p (at level 0).
+  Check # 0 0 _ true.
+  Check fun a => match a with # 0 0 _ _ => 1 | _ => 2 end. (* !! *)
+  End A.
+
+  Module B.
+  Notation "#'" := p (at level 0).
+  Check #' 0 0 true.
+  Check fun a => match a with #' 0 0 _ => 1 | _ => 2 end.
+  End B.
+
+  Module C.
+  Notation "## q" := (@p q) (at level 0, q at level 0).
+  Check ## 0 0 true.
+  Check fun a => match a with ## 0 0 _ => 1 | _ => 2 end.
+  End C.
+
+  Module D.
+  Notation "##' q" := (p q) (at level 0, q at level 0).
+  Check ##' 0 0 true.
+  Check fun a => match a with ##' 0 0 _ => 1 | _ => 2 end.
+  End D.
+
+  Module E.
+  Notation P := @ p.
+  Check P 0 0 _ true.
+  Check fun a => match a with P 0 0 _ _ => 1 | _ => 2 end.
+  End E.
+
+  Module F.
+  Notation P' := p.
+  Check P' 0 0 true.
+  Check fun a => match a with P' 0 0 _ => 1 | _ => 2 end.
+  End F.
+
+  Module G.
+  Notation Q q := (@p q).
+  Check Q 0 0 true.
+  Check fun a => match a with Q 0 0 _ => 1 | _ => 2 end.
+  End G.
+
+  Module H.
+  Notation Q' q := (p q).
+  Check Q' 0 0 true.
+  Check fun a => match a with Q' 0 0 _ => 1 | _ => 2 end.
+  End H.
+
+End AppliedPatternsPrinting.
-- 
cgit v1.2.3


From bf1e15181a2531a106fa643ca8e9233cb889af12 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Nov 2019 21:49:47 +0100
Subject: Fixes #4690: do not allow @f in notations when f is a notation
 variable.

---
 interp/constrintern.ml     | 9 +++++++++
 test-suite/bugs/bug_4690.v | 3 +++
 2 files changed, 12 insertions(+)
 create mode 100644 test-suite/bugs/bug_4690.v

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f68f4e67b9..c39e61083d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -637,6 +637,14 @@ let rec expand_binders ?loc mk bl c =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
+let check_not_notation_variable f ntnvars =
+  (* Check bug #4690 *)
+  match DAst.get f with
+  | GVar id when Id.Map.mem id ntnvars ->
+    user_err (str "Prefix @ is not applicable to notation variables.")
+  | _ ->
+     ()
+
 let option_mem_assoc id = function
   | Some (id',c) -> Id.equal id id'
   | None -> false
@@ -2063,6 +2071,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
             lvar us args ref
         in
+        check_not_notation_variable f ntnvars;
         (* Rem: GApp(_,f,[]) stands for @f *)
         if args = [] then DAst.make ?loc @@ GApp (f,[]) else
           smart_gapp f loc (intern_args env args_scopes (List.map fst args))
diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/bug_4690.v
new file mode 100644
index 0000000000..f50866a990
--- /dev/null
+++ b/test-suite/bugs/bug_4690.v
@@ -0,0 +1,3 @@
+(* Check that @f is not allowed in notation when f is a notation variable *)
+
+Fail Notation "# g" := (@g O) (at level 0).
-- 
cgit v1.2.3


From 12d2e91a9018d2189b041249c440d483c14b5575 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 7 Dec 2019 18:11:52 +0100
Subject: Adding a changelog item.

---
 .../11120-master+refactoring-application-printing.rst    | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 doc/changelog/03-notations/11120-master+refactoring-application-printing.rst

diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
new file mode 100644
index 0000000000..b8bef23f67
--- /dev/null
+++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
@@ -0,0 +1,16 @@
+- **Fixed:** Inheritance of implicit arguments across notations made
+  uniform in parsing and printing. To the exception of notations of
+  the form ``Notation "..." := @foo`` and ``Notation id := @foo`` which
+  inhibit implicit arguments, all notations binding a partially
+  applied constant, as e.g. in ``Notation "..." := (foo args)``,
+  or ``Notation "..." := (@foo args)``, or ``Notation id := (foo args)``, or
+  ``Notation id := (@foo args)``, inherits the remaining implicit arguments
+  (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo
+  Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and
+  `#11091 <https://github.com/coq/coq/pull/11091>`_).
+
+- **Changed:** Interpretation scopes are now always inherited in
+  notations binding a partially applied constant, including for
+  notations binding an expression of the form ``@foo``. The latter was
+  not the case beforehand
+  (part of `#11120 <https://github.com/coq/coq/pull/11120>`_).
-- 
cgit v1.2.3


From 8031bc3963e2c25e04775f5445cc11ad8b5d83e1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 9 Dec 2019 17:10:26 +0100
Subject: Apply and generalize suggestions from Théo.

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
---
 .../11120-master+refactoring-application-printing.rst         | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
index b8bef23f67..7bcd13ae4d 100644
--- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
+++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
@@ -1,16 +1,17 @@
 - **Fixed:** Inheritance of implicit arguments across notations made
   uniform in parsing and printing. To the exception of notations of
-  the form ``Notation "..." := @foo`` and ``Notation id := @foo`` which
+  the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which
   inhibit implicit arguments, all notations binding a partially
-  applied constant, as e.g. in ``Notation "..." := (foo args)``,
-  or ``Notation "..." := (@foo args)``, or ``Notation id := (foo args)``, or
-  ``Notation id := (@foo args)``, inherits the remaining implicit arguments
+  applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`,
+  or :n:`Notation @string := (@@qualid {+ @arg })`, or
+  :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident
+  := (@@qualid {+ @arg })`, inherit the remaining implicit arguments
   (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo
   Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and
   `#11091 <https://github.com/coq/coq/pull/11091>`_).
 
 - **Changed:** Interpretation scopes are now always inherited in
   notations binding a partially applied constant, including for
-  notations binding an expression of the form ``@foo``. The latter was
+  notations binding an expression of the form :n:`@@qualid`. The latter was
   not the case beforehand
   (part of `#11120 <https://github.com/coq/coq/pull/11120>`_).
-- 
cgit v1.2.3


From 2d51333d75bdcce1c1f53830e7303febd7ec2bf4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 12 Dec 2019 21:06:12 +0100
Subject: Update
 doc/changelog/03-notations/11120-master+refactoring-application-printing.rst

Thanks

Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>---
 .../03-notations/11120-master+refactoring-application-printing.rst      | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
index 7bcd13ae4d..7a1d8b508e 100644
--- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
+++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
@@ -1,5 +1,5 @@
 - **Fixed:** Inheritance of implicit arguments across notations made
-  uniform in parsing and printing. To the exception of notations of
+  uniform in parsing and printing. With the exception of notations of
   the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which
   inhibit implicit arguments, all notations binding a partially
   applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`,
-- 
cgit v1.2.3


From 4ef01a6b646b10ed03d40ea8b92d47f05870fcfd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Dec 2019 13:04:55 +0100
Subject: Addressing a changelog comment from Théo Zimmermann.

---
 .../03-notations/11120-master+refactoring-application-printing.rst    | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
index 7a1d8b508e..d95f554766 100644
--- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
+++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
@@ -1,5 +1,5 @@
-- **Fixed:** Inheritance of implicit arguments across notations made
-  uniform in parsing and printing. With the exception of notations of
+- **Fixed:** Parsing and printing consistently handle inheritance of implicit
+  arguments in notations. With the exception of notations of
   the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which
   inhibit implicit arguments, all notations binding a partially
   applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`,
-- 
cgit v1.2.3


From 9e6637326483d1356376bf8bb2fcf2183d3f345b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Feb 2020 09:13:52 +0100
Subject: Documenting inheritance of implicit arguments and scopes in
 notations.

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 27 ++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 7c628e534b..8bfcab0f4e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -417,6 +417,27 @@ identifiers or tokens starting with a single quote are dropped.
    Locate "exists".
    Locate "exists _ .. _ , _".
 
+Inheritance of the properties of arguments of constants bound to a notation
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+If the right-hand side of a notation is a partially applied constant,
+the notation inherits the implicit arguments (see
+:ref:`ImplicitArguments`) and interpretation scopes (see
+:ref:`Scopes`) of the constant. For instance:
+
+.. coqtop:: in reset
+
+   Record R := {dom : Type; op : forall {A}, A -> dom}.
+   Notation "# x" := (@op x) (at level 8).
+
+.. coqtop:: all
+
+   Check fun x:R => # x 3.
+
+As an exception, if the right-hand side is just of the form
+:n:`@@qualid`, this conventionally stops the inheritance of implicit
+arguments (but not of interpretation scopes).
+
 Notations and binders
 ~~~~~~~~~~~~~~~~~~~~~
 
@@ -1415,6 +1436,12 @@ Abbreviations
    denoted expression is performed at definition time. Type checking is
    done only at the time of use of the abbreviation.
 
+   Like for notations, if the right-hand side of an abbreviation is a
+   partially applied constant, the abbreviation inherits the implicit
+   arguments and interpretation scopes of the constant. As an
+   exception, if the right-hand side is just of the form :n:`@@qualid`,
+   this conventionally stops the inheritance of implicit arguments.
+
 .. _numeral-notations:
 
 Numeral notations
-- 
cgit v1.2.3