Merge PR #10061: Print custom grammar entries

Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: jashug

3 files changed, 13 insertions, 2 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 9d972a68f7..c1b9a2b1c6 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -1,5 +1,15 @@
 [< 0 > + < 1 > * < 2 >]
      : nat
+Entry constr:myconstr is
+[ "6" RIGHTA
+  [  ]
+| "5" RIGHTA
+  [ SELF;  "+"; NEXT ]
+| "4" RIGHTA
+  [ SELF;  "*"; NEXT ]
+| "3" RIGHTA
+  [  "<"; constr:operconstr LEVEL "10";  ">" ] ]
+
 [< b > + < b > * < 2 >]
      : nat
 [<< # 0 >>]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 81c64418cb..d1063bfd04 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -9,6 +9,7 @@ Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5).
 Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
 Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
+Print Custom Grammar myconstr.
 
 Axiom a : nat.
 Notation b := a.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 2533a39cc4..d047f7560e 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -151,8 +151,8 @@ Module M16.
   Local Notation "##" := 0 (in custom foo2).
 
   (* Test Print Grammar *)
-  Print Grammar foo.
-  Print Grammar foo2.
+  Print Custom Grammar foo.
+  Print Custom Grammar foo2.
 End M16.
 
 (* Example showing the need for strong evaluation of