New tactic Auto.

[helm.git] / helm / gTopLevel / invokeTactics.mli

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 41cc917b7bed4ed4fc134a9d5d7735ea525383a9..5578c43e519579e4763efe879b058edee2c8deae 100644 (file)
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -59,6 +59,7 @@ module type Callbacks =
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
+    val mqi_handle : MQIConn.handle
   end
 
 module type Tactics =
@@ -101,6 +102,7 @@ module type Tactics =
    val whd_in_scratch : unit -> unit
    val reduce_in_scratch : unit -> unit
    val simpl_in_scratch : unit -> unit
+   val auto : unit -> unit  
  end
 
 module Make (C : Callbacks) : Tactics