first working (?) version of lapply

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 37143ea236603d76f31ff37072786797a758e1b7..4373b9be73927c201d67ba3c09553fcdcfc44959 100644 (file)
--- 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) ->