auto and autogui... some work

[helm.git] / components / tactics / auto.mli

diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli
index e8b2fc038b2be924124f40137fbe8dc788a3c720..eb612ac3a05221fdbe59be4f1deb1239f414fcc8 100644 (file)
--- a/components/tactics/auto.mli
+++ b/components/tactics/auto.mli
@@ -43,12 +43,15 @@ val demodulate_tac :
   ProofEngineTypes.tactic
 
 type auto_status = 
-  Cic.context * (Cic.term * (int * Cic.term) list) list * Cic.term list *
+  Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list * 
+  (int * Cic.term * int) list *
   Cic.term list
 val get_auto_status : unit -> auto_status
 val pause: bool -> unit
 val step : unit -> unit
 val give_hint : int -> unit
-(*
-val cic2grafite : Cic.context -> Cic.metasenv -> Cic.term -> string
-*)
+
+val lambda_close : 
+  ?prefix_name:string -> Cic.term -> Cic.metasenv -> Cic.context -> Cic.term
+
+val pp_proofterm: Cic.term -> string