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

---
 vernac/metasyntax.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'vernac/metasyntax.ml')

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 843296d24e..50914959dc 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -50,10 +50,10 @@ let pr_entry e =
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
-  let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in
+  let gram = Pcoq.find_grammars_by_name name in
   match gram with
-  | None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
-  | Some entries ->
+  | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.")
+  | entries ->
     let pr_one (Pcoq.AnyEntry e) =
       str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++
       pr_entry e
@@ -85,6 +85,8 @@ let pr_grammar = function
       pr_entry Pvernac.Vernac_.gallina_ext
   | name -> pr_registered_grammar name
 
+let pr_custom_grammar name = pr_registered_grammar ("constr:"^name)
+
 (**********************************************************************)
 (* Parse a format (every terminal starting with a letter or a single
    quote (except a single quote alone) must be quoted) *)
-- 
cgit v1.2.3