diff options
Diffstat (limited to 'parsing/ppvernac.mli')
| -rw-r--r-- | parsing/ppvernac.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index 7801de6a2a..6d83ca4741 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -23,4 +23,8 @@ open Topconstr val sep_end : unit -> std_ppcmds +(** Prints a vernac expression *) +val pr_vernac_body : vernac_expr -> std_ppcmds + +(** Prints a vernac expression and closes it with a dot. *) val pr_vernac : vernac_expr -> std_ppcmds |