Updated version 8.8.0+1.gbp069dc3b from 'upstream/8.8.0+1.gbp069dc3b'

with Debian dir 4ca0cfbbc73543887b10ee2613b222f51702e276

1 files changed, 33 insertions, 0 deletions

diff --git a/src/helper.mli b/src/helper.mli
new file mode 100644
index 0000000..400e847
--- /dev/null
+++ b/src/helper.mli
@@ -0,0 +1,33 @@
+(***************************************************************************)
+(*  This is part of aac_tactics, it is distributed under the terms of the  *)
+(*         GNU Lesser General Public License version 3                     *)
+(*              (see file LICENSE for more details)                        *)
+(*                                                                         *)
+(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
+(***************************************************************************)
+
+(** Debugging functions, that can be triggered on a per-file base.  *)
+
+module type CONTROL =			
+sig
+  val debug : bool
+  val time : bool
+  val printing : bool
+end
+module Debug :
+  functor (X : CONTROL) ->
+sig
+      (** {!debug} prints the string and end it with a newline  *)
+      val debug : string -> unit
+      val debug_exception : string -> exn -> unit
+
+      (** {!time} computes the time spent in a function, and then
+      print it using the given format *)
+      val time :
+        ('a -> 'b) -> 'a -> (float -> unit, out_channel, unit) format -> 'b
+	
+      (** {!pr_constr} print a Coq constructor, that can be labelled
+      by a string *)
+      val pr_constr : Environ.env -> Evd.evar_map -> string -> EConstr.constr -> unit
+
+    end