X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=852608d5147d5a5cea305e2c7defdd9c42b86758;hb=0f3081bec320860fbe2208e4d3314629e12a320f;hp=2a73193f6af3cc539048887dc5c738736f2aceb3;hpb=00affce1439533d9b7e581947cefdff93a71ea7b;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 2a73193f6..852608d51 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -57,7 +57,7 @@ let tactic_of_ast = function Tactics.fold ~reduction ~term ~pattern | TacticAst.Fourier _ -> Tactics.fourier | TacticAst.FwdSimpl (_, hyp, names) -> - Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~hyp ~dbd:(MatitaDb.instance ()) + Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp | TacticAst.Generalize (_,pattern,ident) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern