From 4859b79462b9ba591d1fbda769113ffdeda8b4b4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Sep 2014 12:42:17 +0200
Subject: Additional entry tactic_arg in Print Grammar tactic.

---
 toplevel/metasyntax.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e46d3f3775..c674fddb4c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -196,7 +196,9 @@ let pr_grammar = function
       str "Entry binder_tactic is" ++ fnl () ++
       pr_entry Pcoq.Tactic.binder_tactic ++
       str "Entry simple_tactic is" ++ fnl () ++
-      pr_entry Pcoq.Tactic.simple_tactic
+      pr_entry Pcoq.Tactic.simple_tactic ++
+      str "Entry tactic_arg is" ++ fnl () ++
+      pr_entry Pcoq.Tactic.tactic_arg
   | "vernac" ->
       str "Entry vernac is" ++ fnl () ++
       pr_entry Pcoq.Vernac_.vernac ++
-- 
cgit v1.2.3