lapply and fwd improved

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 7239e98e3e2e5ee6ce00b83e2cad8717e4c0a254..1718529cc1e4dd9e0c58531d36549c27b2f306da 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -56,8 +56,8 @@ let tactic_of_ast = function
      in
       Tactics.fold ~reduction ~pattern
   | TacticAst.Fourier _ -> Tactics.fourier
-  | TacticAst.FwdSimpl (_, term) -> 
-     Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
+  | TacticAst.FwdSimpl (_, hyp, names) -> 
+     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~hyp ~dbd:(MatitaDb.instance ())
   | TacticAst.Generalize (_,pattern,ident) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
@@ -69,9 +69,9 @@ let tactic_of_ast = function
   | TacticAst.Intros (_, Some num, names) ->
       PrimitiveTactics.intros_tac ~howmany:num
         ~mk_fresh_name_callback:(namer_of names) ()
-  | TacticAst.LApply (_, to_what, what, ident) ->
+  | TacticAst.LApply (_, how_many, to_what, what, ident) ->
      let names = match ident with None -> [] | Some id -> [id] in
-     Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?to_what what
+     Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what
   | TacticAst.Left _ -> Tactics.left
   | TacticAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
@@ -444,9 +444,8 @@ let disambiguate_tactic status = function
   | TacticAst.Fold (loc,reduction_kind, pattern) ->
      let status, pattern = disambiguate_pattern status pattern in
      status, TacticAst.Fold (loc,reduction_kind, pattern)
-  | TacticAst.FwdSimpl (loc, term) ->
-     let status, term = disambiguate_term status term in
-     status, TacticAst.FwdSimpl (loc, term)  
+  | TacticAst.FwdSimpl (loc, hyp, names) ->
+     status, TacticAst.FwdSimpl (loc, hyp, names)  
   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
   | TacticAst.Generalize (loc,pattern,ident) ->
       let status, pattern = disambiguate_pattern status pattern in
@@ -458,16 +457,14 @@ let disambiguate_tactic status = function
       status, TacticAst.Injection (loc,term)
   | TacticAst.Intros (loc, num, names) ->
       status, TacticAst.Intros (loc, num, names)
-  | TacticAst.LApply (loc, to_what, what, ident) ->
-     let status, to_what =
-      match to_what with
-         None -> status,None
-       | Some to_what -> 
-           let status, to_what = disambiguate_term status to_what in
-           status, Some to_what
+  | TacticAst.LApply (loc, depth, to_what, what, ident) ->
+     let f term (status, to_what) =
+        let status, term = disambiguate_term status term in
+        status, term :: to_what
      in
+     let status, to_what = List.fold_right f to_what (status, []) in 
      let status, what = disambiguate_term status what in
-     status, TacticAst.LApply (loc, to_what, what, ident)
+     status, TacticAst.LApply (loc, depth, to_what, what, ident)
   | TacticAst.Left loc -> status, TacticAst.Left loc
   | TacticAst.LetIn (loc, term, name) ->
       let status, term = disambiguate_term status term in