/usr/lib/coq/user-contrib/AAC_tactics/helper.mli is in libaac-tactics-ocaml-dev 8.6.1-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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
|