X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaEngine.ml;h=852608d5147d5a5cea305e2c7defdd9c42b86758;hb=0f3081bec320860fbe2208e4d3314629e12a320f;hp=1718529cc1e4dd9e0c58531d36549c27b2f306da;hpb=ebaf3deffea9ac78a2b8b2a6c128cc24ad8459ef;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 1718529cc..852608d51 100644
--- 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 (_, hyp, names) -> 
-     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~hyp ~dbd:(MatitaDb.instance ())
+     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
   | TacticAst.Generalize (_,pattern,ident) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
@@ -441,9 +441,10 @@ 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)
+     let status, term = disambiguate_term status term in
+     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