From f20fce1259563f2081fadc62ccab1304bb8161d5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Aug 2015 19:00:59 +0200
Subject: Rich printing of messages.

---
 lib/pp.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index 3b1123a9dc..d034e67617 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -116,7 +116,7 @@ type message_level = Feedback.message_level =
 
 type message = Feedback.message = {
   message_level : message_level;
-  message_content : string;
+  message_content : Xml_datatype.xml;
 }
 
 type logger = message_level -> std_ppcmds -> unit
@@ -154,7 +154,7 @@ val std_logger : logger
 
 val set_logger : logger -> unit
 
-val log_via_feedback : unit -> unit
+val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit
 
 val of_message : message -> Xml_datatype.xml
 val to_message : Xml_datatype.xml -> message
-- 
cgit v1.2.3


From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

---
 lib/pp.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index 3b1123a9dc..2508779e89 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3


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