From d9213c75debd0a6a2bde2aa05bbbcd4b684a52e5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 10 Jun 2005 15:47:37 +0000 Subject: [PATCH] Got rid of a few bugs. --- helm/matita/matitaEngine.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) -> -- 2.39.2