From beb5bdec79ff371f48a478df3c24f2cf9d68aa1f Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 7 May 2019 15:04:04 -0700
Subject: Use Print Custom Grammar to inspect custom entries

---
 test-suite/output/Notations4.out | 10 ++++++++++
 test-suite/output/Notations4.v   |  1 +
 test-suite/success/Notations2.v  |  4 ++--
 3 files changed, 13 insertions(+), 2 deletions(-)

(limited to 'test-suite')

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
-- 
cgit v1.2.3