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.

2 files changed, 30 insertions, 30 deletions

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.