lapply tactic continued

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 522a5157053161e990ebdef8172cef7070e2b5a7..37143ea236603d76f31ff37072786797a758e1b7 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -78,7 +78,7 @@ let tactic_of_ast = function
       else
         EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
   | TacticAst.FwdSimpl (_, term) -> 
-     Tactics.fwd_simpl ~term ~dbd:(MatitaDb.instance ())
+     Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
   | TacticAst.LApply (_, term) ->
      let f (name, term) = Cic.Name name, term in
      Tactics.lapply term