summaryrefslogtreecommitdiff
path: root/AAC_helper.mli
blob: f4e445427e2290412153c20ae394991fc7ea04cd (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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 : string -> Term.constr -> unit

    end