X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.mli;h=57bb26b60ca52a5e2ad6d7f2118fd4fbfc58c16c;hb=57e3de08d963ff08d671c639c0e9990368b86f20;hp=eb612ac3a05221fdbe59be4f1deb1239f414fcc8;hpb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;p=helm.git

diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli
index eb612ac3a..57bb26b60 100644
--- a/helm/software/components/tactics/auto.mli
+++ b/helm/software/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