X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=13dc83f1d02dbba6531d18db4e70d5f0fdbc3321;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e96928988628edb51b686714c9f9a8576f0eae43;hpb=9fb6ab77869badc621194768935c8ddbb39193a0;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index e96928988..13dc83f1d 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -62,6 +62,7 @@ module type Callbacks =
       (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
 ;;
 
@@ -168,7 +169,7 @@ module Make (C: Callbacks) : Tactics =
       in
        handle_refresh_exception
         (fun () ->
-          let metasenv',expr =
+          let metasenv',expr,ugraph = (*TASSI:  FIX THIS*)
            (match term with
            | None -> ()
            | Some t -> (C.term_editor ())#set_term t);
@@ -234,7 +235,7 @@ module Make (C: Callbacks) : Tactics =
                     List.find (function (m,_,_) -> m=metano) metasenv
                    in
                     canonical_context in
-              let (metasenv',expr) =
+              let (metasenv',expr,ugraph) =(* FIX THIS AND *)
                (C.term_editor ())#get_metasenv_and_term
                 canonical_context metasenv
               in
@@ -305,7 +306,7 @@ module Make (C: Callbacks) : Tactics =
     (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 auto = call_tactic (ProofEngine.auto ~dbd:C.dbd)
   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