Merge PR #11326: Refactoring part of #11120 about printing applied global references

Reviewed-by: ejgallego

4 files changed, 774 insertions, 143 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cc0c1e4602..c55e17e7a3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -281,6 +281,17 @@ let get_extern_reference () = !my_extern_reference
 let extern_reference ?loc vars l = !my_extern_reference vars l
 
 (**********************************************************************)
+(* utilities                                                          *)
+
+let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) =
+  match args, subscopes with
+  | [], _ -> []
+  | a :: args, scopt :: subscopes ->
+    (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
+  | a :: args, [] ->
+    (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
+
+(**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
 let add_patt_for_params ind l =
@@ -550,14 +561,14 @@ let is_gvar id c = match DAst.get c with
 | GVar id' -> Id.equal id id'
 | _ -> false
 
-let is_projection nargs = function
-  | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
-    (try
-       let n = Recordops.find_projection_nparams r + 1 in
-         if n <= nargs then Some n
-         else None
-     with Not_found -> None)
-  | _ -> None
+let is_projection nargs r =
+  if not !Flags.in_debugger && not !Flags.raw_print && !print_projections then
+    try
+      let n = Recordops.find_projection_nparams r + 1 in
+      if n <= nargs then Some n
+      else None
+    with Not_found -> None
+  else None
 
 let is_hole = function CHole _ | CEvar _ -> true | _ -> false
 
@@ -569,11 +580,12 @@ let is_needed_for_correct_partial_application tail imp =
 
 exception Expl
 
-(* Implicit args indexes are in ascending order *)
-(* inctx is useful only if there is a last argument to be deduced from ctxt *)
-let explicitize inctx impl (cf,f) args =
-  let impl = if !Constrintern.parsing_explicit then [] else impl in
-  let n = List.length args in
+(* Take a list of arguments starting at position [q] and their implicit status *)
+(* Decide for each implicit argument if it skipped or made explicit *)
+(* If the removal of implicit arguments is not possible, raise [Expl] *)
+(* [inctx] tells if the term is in a context which will enforce the external type *)
+(* [n] is the total number of arguments block to which the [args] belong *)
+let adjust_implicit_arguments inctx n q args impl =
   let rec exprec q = function
     | a::args, imp::impl when is_status_implicit imp ->
         let tail = exprec (q+1) (args,impl) in
@@ -595,10 +607,11 @@ let explicitize inctx impl (cf,f) args =
       (* The non-explicit application cannot be parsed back with the same type *)
       raise Expl
     | [], _ -> []
-  in
+  in exprec q (args,impl)
+
+let extern_projection (cf,f) args impl =
   let ip = is_projection (List.length args) cf in
-  let expl () =
-    match ip with
+  match ip with
     | Some i ->
       (* Careful: It is possible to have declared implicits ending
          before the principal argument *)
@@ -607,33 +620,61 @@ let explicitize inctx impl (cf,f) args =
         with Failure _ -> false
       in
       if is_impl
-      then raise Expl
+      then None
       else
         let (args1,args2) = List.chop i args in
         let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in
-        let args1 = exprec 1 (args1,impl1) in
-        let args2 = exprec (i+1) (args2,impl2) in
-        let ip = Some (List.length args1) in
-          CApp ((ip,f),args1@args2)
-    | None ->
-      let args = exprec 1 (args,impl) in
-        if List.is_empty args then f.CAst.v else
-          match f.CAst.v with
-          | CApp (g,args') ->
-              (* may happen with notations for a prefix of an n-ary
-                 application *)
-              CApp (g,args'@args)
-          | _ -> CApp ((None, f), args) in
-    try expl ()
-    with Expl ->
-      let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
-      let ip = if !print_projections then ip else None in
-        CAppExpl ((ip, f', us), List.map Lazy.force args)
+        Some (i,(args1,impl1),(args2,impl2))
+    | None -> None
 
 let is_start_implicit = function
   | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
   | [] -> false
 
+let extern_record ref args =
+  try
+    if !Flags.raw_print then raise Exit;
+    let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
+    let struc = Recordops.lookup_structure (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 projs = struc.Recordops.s_PROJ in
+    let locals = struc.Recordops.s_PROJKIND in
+    let rec cut args n =
+      if Int.equal n 0 then args
+      else
+        match args with
+        | [] -> raise No_match
+        | _ :: t -> cut t (n - 1) in
+    let args = cut args struc.Recordops.s_EXPECTEDPARAM in
+    let rec ip projs locs args acc =
+      match projs with
+      | [] -> acc
+      | None :: q -> raise No_match
+      | Some c :: q ->
+         match locs with
+         | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
+         | { Recordops.pk_true_proj = false } :: locs' ->
+            (* we don't want to print locals *)
+            ip q locs' args acc
+         | { Recordops.pk_true_proj = true } :: locs' ->
+            match args with
+            | [] -> raise No_match
+            (* we give up since the constructor is not complete *)
+            | arg :: tail ->
+               let arg = Lazy.force arg in
+               let loc = arg.CAst.loc in
+               let ref = extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c) in
+               ip q locs' tail ((ref, arg) :: acc)
+    in
+    Some (List.rev (ip projs locals args []))
+  with
+    | Not_found | No_match | Exit -> None
+
 let extern_global impl f us =
   if not !Constrintern.parsing_explicit && is_start_implicit impl
   then
@@ -641,26 +682,63 @@ let extern_global impl f us =
   else
     CRef (f,us)
 
-let extern_app inctx impl (cf,f) us args =
-  if List.is_empty args then
-    (* If coming from a notation "Notation a := @b" *)
-    CAppExpl ((None, f, us), [])
-  else if not !Constrintern.parsing_explicit &&
-    ((!Flags.raw_print ||
-      (!print_implicits && not !print_implicits_explicit_args)) &&
-     List.exists is_status_implicit impl)
-  then
+(* Implicit args indexes are in ascending order *)
+(* inctx is useful only if there is a last argument to be deduced from ctxt *)
+let extern_applied_ref inctx impl (cf,f) us args =
+  let isproj = is_projection (List.length args) cf in
+  try
+    if not !Constrintern.parsing_explicit &&
+       ((!Flags.raw_print ||
+         (!print_implicits && not !print_implicits_explicit_args)) &&
+        List.exists is_status_implicit impl)
+    then raise Expl;
+    let impl = if !Constrintern.parsing_explicit then [] else impl in
+    let n = List.length args in
+    let ref = CRef (f,us) in
+    let f = CAst.make ref in
+    match extern_projection (cf,f) args impl with
+    (* Try a [t.(f args1) args2] projection-style notation *)
+    | Some (i,(args1,impl1),(args2,impl2)) ->
+      let args1 = adjust_implicit_arguments inctx n 1 args1 impl1 in
+      let args2 = adjust_implicit_arguments inctx n (i+1) args2 impl2 in
+      let ip = Some (List.length args1) in
+      CApp ((ip,f),args1@args2)
+      (* A normal application node with each individual implicit
+         arguments either dropped or made explicit *)
+    | None ->
+      let args = adjust_implicit_arguments inctx n 1 args impl in
+      if args = [] then ref else CApp ((None, f), args)
+  with Expl ->
+  (* A [@f args] node *)
     let args = List.map Lazy.force args in
-    CAppExpl ((is_projection (List.length args) cf,f,us), args)
-  else
-    explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args
+    let isproj = if !print_projections then isproj else None in
+    CAppExpl ((isproj,f,us), args)
 
-let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with
-| [], _ -> []
-| a :: args, scopt :: subscopes ->
-  (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
-| a :: args, [] ->
-  (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
+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 args = syndefargs @ extraargs in
+    if args = [] then cf else CApp ((None, CAst.make cf), args)
+  with Expl ->
+    let args = syndefargs @ List.map Lazy.force extraargs in
+    CAppExpl ((None,f,None), args)
+
+let mkFlattenedCApp (head,args) =
+  match head.CAst.v with
+  | CApp (g,args') ->
+    (* may happen with notations for a prefix of an n-ary application *)
+    (* or after removal of a coercion to funclass *)
+    CApp (g,args'@args)
+  | _ ->
+    CApp ((None, head), args)
+
+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
+    mkFlattenedCApp (f,args)
 
 let extern_args extern env args =
   let map (arg, argscopes) = lazy (extern argscopes env arg) in
@@ -838,56 +916,19 @@ let rec extern inctx scopes vars r =
          | GRef (ref,us) ->
              let subscopes = find_arguments_scope ref in
              let args = fill_arg_scopes args subscopes scopes in
-             begin
-               try
-                 if !Flags.raw_print then raise Exit;
-                 let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
-                 let struc = Recordops.lookup_structure (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 projs = struc.Recordops.s_PROJ in
-                 let locals = struc.Recordops.s_PROJKIND in
-                 let rec cut args n =
-                   if Int.equal n 0 then args
-                   else
-                     match args with
-                     | [] -> raise No_match
-                     | _ :: t -> cut t (n - 1) in
-                 let args = cut args struc.Recordops.s_EXPECTEDPARAM in
-                 let rec ip projs locs args acc =
-                   match projs with
-                     | [] -> acc
-                     | None :: q -> raise No_match
-                     | Some c :: q ->
-                         match locs with
-                           | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
-                           | { Recordops.pk_true_proj = false } :: locs' ->
-                               (* we don't want to print locals *)
-                               ip q locs' args acc
-                           | { Recordops.pk_true_proj = true } :: locs' ->
-                               match args with
-                                 | [] -> raise No_match
-                                     (* we give up since the constructor is not complete *)
-                                 | (arg, scopes) :: tail ->
-                                     let head = extern true scopes vars arg in
-                                     ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc)
-                   in
-                 CRecord (List.rev (ip projs locals args []))
-               with
-                 | Not_found | No_match | Exit ->
-                    let args = extern_args (extern true) vars args in
-                     extern_app inctx
-                       (select_stronger_impargs (implicits_of_global ref))
-                       (Some ref,extern_reference ?loc vars ref) (extern_universes us) args
-             end
-
-         | _       ->
-           explicitize inctx [] (None,sub_extern false scopes vars f)
-             (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
+             let args = extern_args (extern true) vars args in
+             (* Try a "{|...|}" record notation *)
+             (match extern_record ref args with
+             | Some l -> CRecord l
+             | None ->
+             (* Otherwise... *)
+               extern_applied_ref inctx
+                 (select_stronger_impargs (implicits_of_global ref))
+                 (ref,extern_reference ?loc vars ref) (extern_universes us) args)
+         | _ ->
+             let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in
+             let head = sub_extern false scopes vars f in
+             mkFlattenedCApp (head,args))
 
   | GLetIn (na,b,t,c) ->
       CLetIn (make ?loc na,sub_extern false scopes vars b,
@@ -1104,46 +1145,45 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
       let loc = Glob_ops.loc_of_glob_constr t in
       try
         if is_inactive_rule keyrule then raise No_match;
-        (* Adjusts to the number of arguments expected by the notation *)
-        let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with
-          | GApp (f,args), Some n
-              when List.length args >= n ->
+        let f,args =
+          match DAst.get t with
+          | GApp (f,args) -> f,args
+          | _ -> t,[] in
+        let nallargs = List.length args in
+        let argsscopes,argsimpls =
+          match DAst.get f with
+          | GRef (ref,_) ->
+            let subscopes = find_arguments_scope ref in
+            let impls = select_impargs_size nallargs (implicits_of_global ref) in
+            subscopes, impls
+          | _ ->
+            [], [] 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 ->
               let args1, args2 = List.chop n args in
-              let subscopes, impls =
-                match DAst.get f with
-                | GRef (ref,us) ->
-                  let subscopes =
-                    try List.skipn n (find_arguments_scope ref)
-                    with Failure _ -> [] in
-                  let impls =
-                    let impls =
-                      select_impargs_size
-                        (List.length args) (implicits_of_global ref) in
-                    try List.skipn n impls with Failure _ -> [] in
-                  subscopes,impls
-                | _ ->
-                  [], [] 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, subscopes, impls
-          | GApp (f, args), None ->
+              args2, args2scopes, args2impls
+          | None when nallargs > 0 ->
             begin match DAst.get f with
-            | GRef (ref,us) ->
-              let subscopes = find_arguments_scope ref in
-              let impls =
-                  select_impargs_size
-                    (List.length args) (implicits_of_global ref) in
-              f, args, subscopes, impls
+            | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
             end
-          | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], []
-          | _, None -> t, [], [], []
+          | 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 =
           match_notation_constr !print_universes t pat in
         (* Try availability of interpretation ... *)
-        let e =
-          match keyrule with
+        match keyrule with
           | NotationRule (sc,ntn) ->
              (match availability_of_entry_coercion custom (fst ntn) with
              | None -> raise No_match
@@ -1171,22 +1211,25 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                     List.map (fun (bl,(subentry,(scopt,scl))) ->
                       pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
                       binderlists in
-                  insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
+                  let c = make_notation loc ntn (l,ll,bl,bll) in
+                  let c = insert_coercion coercion (insert_delimiters c key) in
+                  let args = fill_arg_scopes args argsscopes allscopes in
+                  let args = extern_args (extern true) vars args in
+                  CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
           | SynDefRule kn ->
              match availability_of_entry_coercion custom InConstrEntrySomeLevel with
              | None -> raise No_match
              | Some coercion ->
               let l =
                 List.map (fun (c,(subentry,(scopt,scl))) ->
-                  extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
+                  extern true (subentry,(scopt,scl@snd scopes)) vars c)
                   terms in
-              let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
-              insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
-        if List.is_empty args then e
-        else
-          let args = fill_arg_scopes args argsscopes allscopes in
-          let args = extern_args (extern true) vars args in
-          CAst.make ?loc @@ explicitize false argsimpls (None,e) args
+              let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in
+              let a = CRef (cf,None) in
+              let args = fill_arg_scopes args argsscopes allscopes in
+              let args = extern_args (extern true) vars args in
+              let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in
+              insert_coercion coercion c
       with
           No_match -> extern_notation allscopes vars t rules
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c699f79351..f4ae5bf676 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1643,7 +1643,7 @@ let drop_notations_pattern looked_for genv =
           | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
           | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-     | CPatCstr (qid, Some expl_pl, pl) ->
+    | CPatCstr (qid, Some expl_pl, pl) ->
       let g = try Nametab.locate qid
               with Not_found ->
               raise (InternalizationError (loc,NotAConstructor qid)) in
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
new file mode 100644
index 0000000000..83dd2f40fb
--- /dev/null
+++ b/test-suite/output/Notations5.out
@@ -0,0 +1,248 @@
+p 0 0 true
+     : 0 = 0 /\ true = true
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p (A:=nat)
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p (A:=nat)
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0 0 true
+     : 0 = 0 /\ true = true
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+f x true
+     : 0 = 0 /\ true = true
+f x (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+f x (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+@f nat
+     : forall a1 a2 : nat,
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+@f
+     : forall (A : Type) (a1 a2 : A),
+       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
+x.(f) true
+     : 0 = 0 /\ true = true
+x.(f) (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+x.(f) (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+@f nat
+     : forall a1 a2 : nat,
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+@f
+     : forall (A : Type) (a1 a2 : A),
+       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
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+p
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+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
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p 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
+     : 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
+u
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+u 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+u 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+@u nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@u nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+u 0 0 true
+     : 0 = 0 /\ true = true
+u 0 0 true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+v 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+v 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+##
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+##
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+## 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
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool) 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
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+##
+     : 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
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 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
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p 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 (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 = true
+## 0 0 (B:=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 (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 = true
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
new file mode 100644
index 0000000000..b3bea929ba
--- /dev/null
+++ b/test-suite/output/Notations5.v
@@ -0,0 +1,340 @@
+Module AppliedTermsPrinting.
+
+(* Test different printing paths for applied terms *)
+
+  Module InferredGivenImplicit.
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Check p 0 0 true.
+  (* p 0 0 true *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check p 0.
+  (* p 0 *)
+  Check @p _ 0 0 bool.
+  (* p 0 0 (B:=bool) *)
+  Check p 0 0 (B:=bool).
+  (* p 0 0 (B:=bool) *)
+  Check @p nat.
+  (* p (A:=nat) *)
+  Check p (A:=nat).
+  (* p (A:=nat) *)
+  Check @p _ 0 0.
+  (* @p nat 0 0 *)
+  Check @p.
+  (* @p *)
+
+  Unset Printing Implicit Defensive.
+  Check @p _ 0 0 bool.
+  (* p 0 0 *)
+  Check @p nat.
+  (* p *)
+  Set Printing Implicit Defensive.
+  End InferredGivenImplicit.
+
+  Module ManuallyGivenImplicit.
+  Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b.
+
+  Check p 0 0 true.
+  (* p 0 0 true *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check p 0.
+  (* p 0 *)
+  Check @p _ 0 0 bool.
+  (* p 0 0 *)
+  Check p 0 0 (B:=bool).
+  (* p 0 0 *)
+  Check @p nat.
+  (* p *)
+  Check p (A:=nat).
+  (* p *)
+  Check @p _ 0 0.
+  (* @p nat 0 0 *)
+  Check @p.
+  (* @p *)
+
+  End ManuallyGivenImplicit.
+
+  Module ProjectionWithImplicits.
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Record T {A} (a1 a2:A) := { f : forall B (b:B), a1 = a2 /\ b = b }.
+  Parameter x : T 0 0.
+  Check f x true.
+  (* f x true *)
+  Check @f _ _ _ x bool.
+  (* f x (B:=bool) *)
+  Check f x (B:=bool).
+  (* f x (B:=bool) *)
+  Check @f nat.
+  (* @f nat *)
+  Check @f _ 0 0.
+  (* f (a1:=0) (a2:=0) *)
+  Check f (a1:=0) (a2:=0).
+  (* f (a1:=0) (a2:=0) *)
+  Check @f.
+  (* @f *)
+
+  Unset Printing Implicit Defensive.
+  Check f (a1:=0) (a2:=0).
+  (* f *)
+  Set Printing Implicit Defensive.
+
+  Set Printing Projections.
+
+  Check x.(f) true.
+  (* x.(f) true *)
+  Check x.(@f _ _ _) bool.
+  (* x.(f) (B:=bool) *)
+  Check x.(f) (B:=bool).
+  (* x.(f) (B:=bool) *)
+  Check @f nat.
+  (* @f nat *)
+  Check @f _ 0 0.
+  (* f (a1:=0) (a2:=0) *)
+  Check f (a1:=0) (a2:=0).
+  (* f (a1:=0) (a2:=0) *)
+  Check @f.
+  (* @f *)
+
+  Unset Printing Implicit Defensive.
+  Check f (a1:=0) (a2:=0).
+  (* f *)
+
+  End ProjectionWithImplicits.
+
+  Module AtAbbreviationForApplicationHead.
+
+  Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b.
+
+  Notation u := @p.
+
+  Check u _.
+  (* p *)
+  Check p.
+  (* p *)
+  Check @p.
+  (* u *)
+  Check u.
+  (* u *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check u nat 0 0 bool.
+  (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *)
+  Check u nat 0 0.
+  (* @p nat 0 0 *)
+  Check @p nat 0 0.
+  (* @p nat 0 0 *)
+
+  End AtAbbreviationForApplicationHead.
+
+  Module AbbreviationForApplicationHead.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation u := p.
+
+  Check p.
+  (* u *)
+  Check @p.
+  (* u -- BUG *)
+  Check @u.
+  (* u -- BUG *)
+  Check u.
+  (* u *)
+  Check p 0 0.
+  (* u 0 0 *)
+  Check u 0 0.
+  (* u 0 0 *)
+  Check @p nat 0 0.
+  (* @u nat 0 0 *)
+  Check @u nat 0 0.
+  (* @u nat 0 0 *)
+  Check p 0 0 true.
+  (* u 0 0 true *)
+  Check u 0 0 true.
+  (* u 0 0 true *)
+
+  End AbbreviationForApplicationHead.
+
+  Module AtAbbreviationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation v := (@p _ 0).
+
+  Check v.
+  (* v *)
+  Check p 0 0.
+  (* v 0 *)
+  Check v 0.
+  (* v 0 *)
+  Check v 0 true.
+  (* v 0 (B:=bool) true -- BUG *)
+  Check @p nat 0.
+  (* v *)
+  Check @p nat 0 0.
+  (* @v 0 *)
+  Check @v 0.
+  (* @v 0 *)
+  Check @p nat 0 0 bool.
+  (* v 0 (B:=bool) *)
+
+  End AtAbbreviationForPartialApplication.
+
+  Module AbbreviationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation v := (p 0).
+
+  Check v.
+  (* v *)
+  Check p 0 0.
+  (* v 0 *)
+  Check v 0.
+  (* v 0 *)
+  Check v 0 true.
+  (* v 0 (B:=bool) true -- BUG *)
+  Check @p nat 0.
+  (* v *)
+  Check @p nat 0 0.
+  (* @v 0 *)
+  Check @v 0.
+  (* @v 0 *)
+  Check @p nat 0 0 bool.
+  (* v 0 (B:=bool) *)
+
+  End AbbreviationForPartialApplication.
+
+  Module NotationForHeadApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "##" := p (at level 0).
+
+  Check p.
+  (* ## *)
+  Check ##.
+  (* ## *)
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  Check p 0 0.
+  (* ## 0 0 *)
+  Check ## 0 0.
+  (* ## 0 0 *)
+  Check p 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check ## 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check p 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+
+  End NotationForHeadApplication.
+
+  Module AtNotationForHeadApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "##" := @p (at level 0).
+
+  Check p.
+  (* p *)
+  Check @p.
+  (* ## *)
+  Check ##.
+  (* ## *)
+  Check p 0.
+  (* p 0 -- why not "## nat 0" *)
+  Check ## nat 0.
+  (* p 0 *)
+  Check ## nat 0 0.
+  (* @p nat 0 0 *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check ## nat 0 0 _.
+  (* p 0 0 *)
+  Check ## nat 0 0 bool.
+  (* p 0 0 (B:=bool) *)
+  Check ## nat 0 0 bool true.
+  (* p 0 0 true *)
+
+  End AtNotationForHeadApplication.
+
+  Module NotationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "## q" := (p q) (at level 0, q at level 0).
+
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  (* Check ## 0 0. *)
+  (* Anomaly *)
+  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 *)
+  Check ## 0 0 bool true.
+  (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *)
+
+  End NotationForPartialApplication.
+
+  Module AtNotationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "## q" := (@p _ q) (at level 0, q at level 0).
+
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  (* Check ## 0 0. *)
+  (* Anomaly *)
+  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 *)
+  Check ## 0 0 bool true.
+  (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *)
+
+  End AtNotationForPartialApplication.
+
+End AppliedTermsPrinting.