X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=4373b9be73927c201d67ba3c09553fcdcfc44959;hb=8c5a76439368f52a7df7c7b524c726b1f9d4eb39;hp=37143ea236603d76f31ff37072786797a758e1b7;hpb=98c386d8d12a2fe4d64017e0b1bf684b22fe6423;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 37143ea23..4373b9be7 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -79,9 +79,8 @@ let tactic_of_ast = function
         EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
   | TacticAst.FwdSimpl (_, term) -> 
      Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
-  | TacticAst.LApply (_, term) ->
-     let f (name, term) = Cic.Name name, term in
-     Tactics.lapply term
+  | TacticAst.LApply (_, to_what, what) ->
+     Tactics.lapply ?to_what what
 
 let eval_tactical status tac =
   let apply_tactic tactic =
@@ -452,9 +451,13 @@ let disambiguate_tactic status = function
   | TacticAst.FwdSimpl (loc, term) ->
      let status, term = disambiguate_term status term in
      status, TacticAst.FwdSimpl (loc, term)  
-  | TacticAst.LApply (loc, term) ->
-     let status, term = disambiguate_term status term in
-     status, TacticAst.LApply (loc, term)
+  | TacticAst.LApply (loc, Some to_what, what) ->
+     let status, to_what = disambiguate_term status to_what in
+     let status, what = disambiguate_term status what in
+     status, TacticAst.LApply (loc, Some to_what, what)
+  | TacticAst.LApply (loc, None, what) ->
+     let status, what = disambiguate_term status what in
+     status, TacticAst.LApply (loc, None, what)
 
 let rec disambiguate_tactical status = function 
   | TacticAst.Tactic (loc, tactic) ->