1signature hhReconstruct =
2sig
3
4  include Abbrev
5
6  (* Settings *)
7  val reconstruct_flag : bool ref
8  val minimization_timeout : real ref
9  val reconstruction_timeout : real ref
10
11  (* Read output of ATP *)
12  val get_lemmas : (string * string) -> string list option
13
14  (* Reconstruction *)
15  val mk_metis_call  : string list -> string
16  val hh_reconstruct : string list -> goal -> (string * tactic)
17
18end
19