11 files changed, 34 insertions, 8 deletions

diff --git a/doc/changelog/03-notations/10061-print-custom-grammar.rst b/doc/changelog/03-notations/10061-print-custom-grammar.rst
new file mode 100644
index 0000000000..8786c7ce6b
--- /dev/null
+++ b/doc/changelog/03-notations/10061-print-custom-grammar.rst
@@ -0,0 +1,4 @@
+- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar`
+  (`#10061 <https://github.com/coq/coq/pull/10061>`_,
+  fixes `#9681 <http://github.com/coq/coq/pull/9681>`_,
+  by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index ac079ea7d5..edec13f681 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -840,10 +840,11 @@ gives a way to let any arbitrary expression which is not handled by the
 custom entry ``expr`` be parsed or printed by the main grammar of term
 up to the insertion of a pair of curly brackets.
 
-.. cmd:: Print Grammar @ident.
+.. cmd:: Print Custom Grammar @ident.
+   :name: Print Custom Grammar
 
-   This displays the state of the grammar for terms and grammar for
-   patterns associated to the custom entry :token:`ident`.
+   This displays the state of the grammar for terms associated to
+   the custom entry :token:`ident`.
 
 Summary
 ~~~~~~~
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
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 59d2a66259..94d4ed80d1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1003,6 +1003,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Grammar"; ent = IDENT ->
           (* This should be in "syntax" section but is here for factorization*)
 	  { PrintGrammar ent }
+      | IDENT "Custom"; IDENT "Grammar"; ent = IDENT ->
+          (* Should also be in "syntax" section *)
+          { PrintCustomGrammar ent }
       | IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir }
       | IDENT "Modules" ->
           { user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") }
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) *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 38dbdf7e41..6435df23c7 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -57,6 +57,7 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
 (** Print the Camlp5 state of a grammar *)
 
 val pr_grammar : string -> Pp.t
+val pr_custom_grammar : string -> Pp.t
 
 val check_infix_modifiers : syntax_modifier list -> unit
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 889dbafabd..f2332bab8b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -476,6 +476,8 @@ open Pputils
       keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
     | PrintGrammar ent ->
       keyword "Print Grammar" ++ spc() ++ str ent
+    | PrintCustomGrammar ent ->
+      keyword "Print Custom Grammar" ++ spc() ++ str ent
     | PrintLoadPath dir ->
       keyword "Print LoadPath" ++ pr_opt DirPath.print dir
     | PrintModules ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 279d4f0935..c7795602aa 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1885,6 +1885,7 @@ let vernac_print ~(pstate : Proof_global.t option) ~atts =
   | PrintSectionContext qid -> print_sec_context_typ env sigma qid
   | PrintInspect n -> inspect env sigma n
   | PrintGrammar ent -> Metasyntax.pr_grammar ent
+  | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent
   | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
   | PrintModules -> print_modules ()
   | PrintModule qid -> print_module qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 34a9b9394a..6a51fdfe59 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -29,6 +29,7 @@ type printable =
   | PrintSectionContext of qualid
   | PrintInspect of int
   | PrintGrammar of string
+  | PrintCustomGrammar of string
   | PrintLoadPath of DirPath.t option
   | PrintModules
   | PrintModule of qualid