X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=e96928988628edb51b686714c9f9a8576f0eae43;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=5f01eff9f489d967fc9526eb4add5c3b71be4e80;hpb=fe1e7e151af9690f312259a4c1c969a1388bee5f;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 5f01eff9f..e96928988 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -61,6 +61,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
 ;;
 
@@ -104,6 +105,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 =
@@ -297,11 +299,13 @@ module Make (C: Callbacks) : Tactics =
      | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected"))
 
 
+
   let intros =
    call_tactic
     (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
   let exact = call_tactic_with_input ProofEngine.exact
   let apply = call_tactic_with_input ProofEngine.apply
+  let auto = call_tactic (ProofEngine.auto C.mqi_handle)
   let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
   let elimtype = call_tactic_with_input ProofEngine.elim_type
   let whd = call_tactic_with_goal_inputs ProofEngine.whd