diff options
| author | Hugo Herbelin | 2016-04-09 11:56:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-09 18:25:59 +0200 |
| commit | ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 (patch) | |
| tree | 70cd706240e86e9ecf3fe3ce1f99eee6f896381a /lib/pp.mli | |
| parent | bb43730ac876b8de79967090afa50f00858af6d5 (diff) | |
In pr_clauses, do not print a leading space by default so that it can
be used in the generic printer for tactics.
Allows e.g. to print "symmetry in H" correctly after its move to
TACTIC EXTEND.
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 015151bc90..2e4d029749 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -199,6 +199,9 @@ val pr_bar : unit -> std_ppcmds val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds (** Adds a space in front of its argument. *) +val pr_non_empty_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds +(** Adds a space in front of its argument if non empty. *) + val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds (** Inner object preceded with a space if [Some], nothing otherwise. *) |