New test.

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 7239e98e3e2e5ee6ce00b83e2cad8717e4c0a254..2a73193f6af3cc539048887dc5c738736f2aceb3 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -46,7 +46,7 @@ let tactic_of_ast = function
   | TacticAst.Exact (_, term) -> Tactics.exact term
   | TacticAst.Exists _ -> Tactics.exists
   | TacticAst.Fail _ -> Tactics.fail
-  | TacticAst.Fold (_, reduction_kind, pattern) ->
+  | TacticAst.Fold (_, reduction_kind, term, pattern) ->
      let reduction =
       match reduction_kind with
        | `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
@@ -54,10 +54,10 @@ let tactic_of_ast = function
        | `Simpl -> ProofEngineReduction.simpl
        | `Whd -> CicReduction.whd ~delta:false ~subst:[]
      in
-      Tactics.fold ~reduction ~pattern
+      Tactics.fold ~reduction ~term ~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])
@@ -441,12 +441,12 @@ let disambiguate_tactic status = function
       status, TacticAst.ElimType (loc, cic)
   | TacticAst.Exists loc -> status, TacticAst.Exists loc 
   | TacticAst.Fail loc -> status,TacticAst.Fail loc
-  | TacticAst.Fold (loc,reduction_kind, pattern) ->
+  | TacticAst.Fold (loc,reduction_kind, term, 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)  
+     status, TacticAst.Fold (loc,reduction_kind, term, pattern)
+  | 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 +458,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