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/success/Notations2.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite/success')

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