diff options
author | Benjamin Barenblat <bbaren@google.com> | 2019-02-13 20:40:51 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@google.com> | 2019-02-13 20:40:51 -0500 |
commit | 8018e923c75eb5504310864f821972f794b7d554 (patch) | |
tree | 88a55f7c23fcbbea0ff80e406555292049b48dec /helper.mli | |
parent | 76f9b4cdc5693a6313961e2f91b39ba311857e72 (diff) |
New upstream version 8.8.0+1.gbp069dc3bupstream/8.8.0+1.gbp069dc3bupstream
Diffstat (limited to 'helper.mli')
-rw-r--r-- | helper.mli | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/helper.mli b/helper.mli deleted file mode 100644 index f4e4454..0000000 --- a/helper.mli +++ /dev/null @@ -1,33 +0,0 @@ -(***************************************************************************) -(* 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 : string -> Term.constr -> unit - - end |