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 3d3e10456..b5367048a 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -878,7 +878,7 @@ let rec pr_vernac = function | PrintHintDb -> str"Print Hint *" | PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s | PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s - | PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt + | PrintUniverses fopt -> str"Print Universes" ++ pr_opt str fopt | PrintName qid -> str"Print" ++ spc() ++ pr_smart_global qid | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid |