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.

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.