diff options
Diffstat (limited to 'vernac/metasyntax.ml')
-rw-r--r-- | vernac/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 6c3dfec7d..1bb9e0da1 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -80,8 +80,8 @@ let pr_grammar = function | "pattern" -> pr_entry Pcoq.Constr.pattern | "vernac" -> - str "Entry vernac is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.vernac ++ + str "Entry vernac_control is" ++ fnl () ++ + pr_entry Pcoq.Vernac_.vernac_control ++ str "Entry command is" ++ fnl () ++ pr_entry Pcoq.Vernac_.command ++ str "Entry syntax is" ++ fnl () ++ |