added support for goal patterns

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a55930fa52299446a5e9167f1f521b5e6081302a..14eab882c80dc39f942def9de4d0a052e962c38f 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -49,8 +49,9 @@ let tactic_of_ast = function
       Tactics.elim_intros term
   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
-  | TacticAst.Auto (_,num) -> 
-      AutoTactic.auto_tac ~num (MatitaDb.instance ())
+  | TacticAst.Auto (_,depth) -> 
+(*       AutoTactic.auto_tac ~num (MatitaDb.instance ()) *)
+      AutoTactic.auto_tac_new ?depth ~dbd:(MatitaDb.instance ()) ()
   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
 (*
   (* TODO Zack a lot more of tactics to be implemented here ... *)
@@ -211,11 +212,11 @@ let eval_coercion status coercion =
   let context = [] in 
   let src_uri = 
     let ty_src = CicReduction.whd context ty_src in
-    UriManager.uri_of_string (CicUtil.uri_of_term ty_src) 
+     CicUtil.uri_of_term ty_src
   in
   let tgt_uri = 
     let ty_tgt = CicReduction.whd context ty_tgt in
-    UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) 
+     CicUtil.uri_of_term ty_tgt
   in
   let new_coercions =
     (* also adds them to the Db *)
@@ -287,7 +288,7 @@ let eval_command status cmd =
           {status with aliases = 
             DisambiguateTypes.Environment.add 
               (DisambiguateTypes.Id id) 
-              ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri)) 
+              ("boh?",(fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
               status.aliases }
       | TacticAst.Symbol_alias (symb, instance, desc) ->
           {status with aliases =