Got rid of a few bugs.

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 8aae7633a9222fd8f8dc86b0a3d737369827492b..f16b0226678d9ea525c63e5c2bbc6f93e3a36303 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -50,7 +50,7 @@ let tactic_of_ast = function
   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
   | TacticAst.Auto (_,num) -> 
-      AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
+      AutoTactic.auto_tac ~num (MatitaDb.instance ())
   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
 (*
   (* TODO Zack a lot more of tactics to be implemented here ... *)
@@ -63,7 +63,7 @@ let tactic_of_ast = function
   | TacticAst.Replace_pattern of 'term pattern * 'term
 *)
   | TacticAst.LetIn (loc,term,name) ->
-      Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name])
+      Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
   | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
       ProofEngineTypes.mk_tactic 
       (fun (((_,metasenv,_,_),goal) as status) ->