Merge PR #11120: Refactoring code for application printing + fixing #11091 (inconsistencies in parsing/printing notations to partial applications)

Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle

12 files changed, 360 insertions, 139 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
new file mode 100644
index 0000000000..d95f554766
--- /dev/null
+++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
@@ -0,0 +1,17 @@
+- **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 })`,
+  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 :n:`@@qualid`. The latter was
+  not the case beforehand
+  (part of `#11120 <https://github.com/coq/coq/pull/11120>`_).
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
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 38dc10a9b3..4ec9f17c71 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
@@ -473,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) ->
@@ -496,10 +508,14 @@ 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
+                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
@@ -516,10 +532,14 @@ 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
+          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
@@ -742,7 +762,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 +782,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
@@ -1207,24 +1229,21 @@ 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
-          | None when nallargs > 0 ->
+              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
             | 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
-          | None -> t, [], [], []
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1cfd50e26e..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
@@ -1071,11 +1079,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
@@ -1659,10 +1667,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;
@@ -1680,7 +1689,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 +1789,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.");
@@ -2054,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))
@@ -2070,9 +2088,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/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/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).
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b870fa6f6f..53ad8a9612 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -107,14 +107,15 @@ 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 => 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 c5b4d6f291..f59306c454 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -78,11 +78,11 @@ 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 ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-p
+u ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -90,23 +90,23 @@ u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-p 0 0
+u nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+u nat 0 0 bool
      : 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
 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
@@ -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,15 +188,15 @@ 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
 ## 0 0 (B:=bool)
      : forall b : bool, 0 = 0 /\ b = b
-p
+## ?A
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
@@ -204,45 +204,109 @@ 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
+## nat 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-p 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
-p 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+## nat 0 0 ?B
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0
+## nat 0 0 bool
      : forall b : bool, 0 = 0 /\ b = b
-p 0 0 true
+## nat 0 0 bool 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
+## 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)
      : 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
+## 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)
      : 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 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 b3bea929ba..09d5e31c48 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 ?A *)
   Check p.
-  (* p *)
+  (* u ?A *)
   Check @p.
   (* u *)
   Check u.
   (* u *)
   Check p 0 0.
-  (* p 0 0 *)
+  (* u nat 0 0 ?B *)
   Check u nat 0 0 bool.
-  (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *)
+  (* u nat 0 0 bool *)
   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.
 
@@ -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.
@@ -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).
@@ -263,25 +263,25 @@ Module AppliedTermsPrinting.
   Notation "##" := @p (at level 0).
 
   Check p.
-  (* p *)
+  (* ## ?A *)
   Check @p.
   (* ## *)
   Check ##.
   (* ## *)
   Check p 0.
-  (* p 0 -- why not "## nat 0" *)
+  (* ## nat 0 *)
   Check ## nat 0.
-  (* p 0 *)
+  (* ## nat 0 *)
   Check ## nat 0 0.
-  (* @p nat 0 0 *)
+  (* ## nat 0 0 *)
   Check p 0 0.
-  (* p 0 0 *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 _.
-  (* p 0 0 *)
+  (* ## nat 0 0 ?B *)
   Check ## nat 0 0 bool.
-  (* p 0 0 (B:=bool) *)
+  (* ## nat 0 0 bool *)
   Check ## nat 0 0 bool true.
-  (* p 0 0 true *)
+  (* ## nat 0 0 bool true *)
 
   End AtNotationForHeadApplication.
 
@@ -298,16 +298,16 @@ Module AppliedTermsPrinting.
   (* ## 0 *)
   Check ## 0.
   (* ## 0 *)
-  (* Check ## 0 0. *)
-  (* Anomaly *)
+  Check ## 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 (B:=bool) true -- BUG B should not be displayed *)
-  Check ## 0 0 bool true.
-  (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *)
+  (* ## 0 0 true *)
+  Check ## 0 0 true.
+  (* ## 0 0 true *)
 
   End NotationForPartialApplication.
 
@@ -324,17 +324,75 @@ Module AppliedTermsPrinting.
   (* ## 0 *)
   Check ## 0.
   (* ## 0 *)
-  (* Check ## 0 0. *)
-  (* Anomaly *)
+  Check ## 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 (B:=bool) true -- BUG B should not be displayed *)
-  Check ## 0 0 bool true.
-  (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *)
+  (* ## 0 0 true *)
+  Check ## 0 0 true.
+  (* ## 0 0 true *)
 
   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.
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.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index b26e725d9b..f166a53256 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,18 +62,18 @@ 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 fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
+Check # 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with # 0 y 0 => 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 fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
+Check ## 0%bool 0 0 : prod' bool bool.
+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).
@@ -86,10 +86,10 @@ 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 fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
+Check ##### 0 0 0 : prod' bool bool.
+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 *)
@@ -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.