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.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/pp.ml')

diff --git a/lib/pp.ml b/lib/pp.ml
index 9a833ae225..c7cf9b8d0e 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -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
 
-- 
cgit v1.2.3