An API for info traces.

1 files changed, 13 insertions, 0 deletions

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 293d99fdcf..934a445743 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -145,6 +145,7 @@ type +'a tactic
 val apply : Environ.env -> 'a tactic -> proofview -> 'a
                                                    * proofview
                                                    * (bool*Goal.goal list*Goal.goal list)
+                                                   * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
 
@@ -474,6 +475,18 @@ module Refine : sig
 end
 
 
+(** {6 Trace} *)
+
+module Trace : sig
+
+  val log : Proofview_monad.lazy_msg -> unit tactic
+  val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
+
+  val pr_info : Proofview_monad.Info.tree -> Pp.std_ppcmds
+
+end
+
+
 (** {6 Non-logical state} *)
 
 (** The [NonLogical] module allows the execution of effects (including