From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Jun 2005 15:47:37 +0000 (+0000)
Subject: Got rid of a few bugs.
X-Git-Tag: PRE_STORAGE~73
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d9213c75debd0a6a2bde2aa05bbbcd4b684a52e5;p=helm.git

Got rid of a few bugs.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 8aae7633a..f16b02266 100644
--- 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) ->