diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-03 12:42:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-03 12:42:17 +0200 |
| commit | 4859b79462b9ba591d1fbda769113ffdeda8b4b4 (patch) | |
| tree | 9c71d799b24945b90202950d0fbc00e46b3af5d1 | |
| parent | e4e2b237da0f40d01c30f3110d2d4424edc70204 (diff) | |
Additional entry tactic_arg in Print Grammar tactic.
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e46d3f377..c674fddb4 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 ++ |