diff options
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 33c7654d2..a3eed62b7 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -878,7 +878,7 @@ let rec pr_vernac = function str"Print Section" ++ spc() ++ Libnames.pr_reference s | PrintGrammar ent -> str"Print Grammar" ++ spc() ++ str ent - | PrintLoadPath -> str"Print LoadPath" + | PrintLoadPath dir -> str"Print LoadPath" ++ pr_opt pr_dirpath dir | PrintModules -> str"Print Modules" | PrintMLLoadPath -> str"Print ML Path" | PrintMLModules -> str"Print ML Modules" |