summaryrefslogtreecommitdiff
path: root/helper.ml
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@google.com>2019-02-13 20:40:51 -0500
committerGravatar Benjamin Barenblat <bbaren@google.com>2019-02-13 20:40:51 -0500
commit8018e923c75eb5504310864f821972f794b7d554 (patch)
tree88a55f7c23fcbbea0ff80e406555292049b48dec /helper.ml
parent76f9b4cdc5693a6313961e2f91b39ba311857e72 (diff)
New upstream version 8.8.0+1.gbp069dc3bupstream/8.8.0+1.gbp069dc3bupstream
Diffstat (limited to 'helper.ml')
-rw-r--r--helper.ml41
1 files changed, 0 insertions, 41 deletions
diff --git a/helper.ml b/helper.ml
deleted file mode 100644
index 636b17f..0000000
--- a/helper.ml
+++ /dev/null
@@ -1,41 +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. *)
-(***************************************************************************)
-
-module type CONTROL = sig
- val debug : bool
- val time : bool
- val printing : bool
-end
-
-module Debug (X : CONTROL) = struct
- open X
- let debug x =
- if debug then
- Printf.printf "%s\n%!" x
-
-
- let time f x fmt =
- if time then
- let t = Sys.time () in
- let r = f x in
- Printf.printf fmt (Sys.time () -. t);
- r
- else f x
-
- let pr_constr msg constr =
- if printing then
- ( Feedback.msg_notice (Pp.str (Printf.sprintf "=====%s====" msg));
- Feedback.msg_notice (Printer.pr_constr constr);
- )
-
-
- let debug_exception msg e =
- debug (msg ^ (Printexc.to_string e))
-
-
-end