ocaml 3.09 transition

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

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 41cc917b7bed4ed4fc134a9d5d7735ea525383a9..993199fe4b9fa70866297dc9aef8e40a8e79b715 100644 (file)
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -59,6 +59,8 @@ 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
+    val dbd:Mysql.dbd
   end
 
 module type Tactics =
@@ -101,6 +103,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