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.ml | |
| 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.ml')
| -rw-r--r-- | lib/pp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -518,6 +518,7 @@ let pr_comma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () let pr_arg pr x = spc () ++ pr x +let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x |