diff options
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 -> |