Allowing to extend the Print Grammar command generically.

We also move the Ltac-specific grammar to its folder.

1 files changed, 12 insertions, 0 deletions

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 2d7b7bf137..d05beb3926 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -511,3 +511,15 @@ let print_ltacs () =
     hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
   in
   Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
+
+(** Grammar *)
+
+let () =
+  let open Metasyntax in
+  let entries = [
+    AnyEntry Pcoq.Tactic.tactic_expr;
+    AnyEntry Pcoq.Tactic.binder_tactic;
+    AnyEntry Pcoq.Tactic.simple_tactic;
+    AnyEntry Pcoq.Tactic.tactic_arg;
+  ] in
+  register_grammar "tactic" entries