fix

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 2ac69a57502a31b0487f89b39caec8ac46921355..d9297bce5d517c20182a8648c220995597171a08 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -123,6 +123,11 @@ let tactic_of_ast = function
         EqualityTactics.rewrite_tac ~term:t 
       else
         EqualityTactics.rewrite_back_tac ~term:t
+  | TacticAst.FwdSimpl (_, name) -> 
+     Tactics.fwd_simpl ~hyp:(Cic.Name name) ~dbd:(MatitaDb.instance ())
+  | TacticAst.LApply (_, term, substs) ->
+     let f (name, term) = Cic.Name name, term in
+     Tactics.lapply ~substs:(List.map f substs) term
   | _ -> assert false
 
 let eval_tactical status tac =
@@ -488,6 +493,16 @@ let disambiguate_tactic status = function
   | TacticAst.Split loc -> status, TacticAst.Split loc
   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
+  | TacticAst.FwdSimpl (loc, name) -> status, TacticAst.FwdSimpl (loc, name)  
+  | TacticAst.LApply (loc, term, substs) ->
+     let f (status, substs) (name, term) =
+        let status, term = disambiguate_term status term in
+       status, (name, term) :: substs
+     in
+     let status, term = disambiguate_term status term in
+     let status, substs = List.fold_left f (status, []) substs in 
+     status, TacticAst.LApply (loc, term, substs)
+  
   | x -> 
       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
       assert false