From ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 9 Apr 2016 11:56:53 +0200
Subject: 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.
---
 lib/pp.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'lib/pp.mli')

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. *)
 
-- 
cgit v1.2.3