diff options
Diffstat (limited to 'printing')
-rw-r--r-- | printing/ppvernac.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 427317a45..d8ddb275d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -920,6 +920,9 @@ let rec pr_vernac = function | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid | LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid in str"Locate" ++ spc() ++ pr_locate loc + | VernacRegister (id, RegisterInline) -> + hov 2 + (str "Register Inline" ++ spc() ++ pr_lident id) | VernacComments l -> hov 2 (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) |