added pruning option in autogui

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

diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli
index eb612ac3a05221fdbe59be4f1deb1239f414fcc8..57bb26b60ca52a5e2ad6d7f2118fd4fbfc58c16c 100644 (file)
--- a/components/tactics/auto.mli
+++ b/components/tactics/auto.mli
@@ -50,8 +50,11 @@ val get_auto_status : unit -> auto_status
 val pause: bool -> unit
 val step : unit -> unit
 val give_hint : int -> unit
+val give_prune_hint : int -> unit
 
 val lambda_close : 
   ?prefix_name:string -> Cic.term -> Cic.metasenv -> Cic.context -> Cic.term
 
 val pp_proofterm: Cic.term -> string 
+val revision : string (* svn revision *)
+val size_and_depth : Cic.context -> Cic.metasenv -> Cic.term -> int * int