X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FreductionTactics.ml;h=54b439b25ae40ef31a0fc0c8356eadec95774383;hb=370f967a478c116fcc85a81c7953363b4351a2e9;hp=0080e4571255062d85a4b91be1bdb8b2e701a2f4;hpb=989a5444a5162ba9259858a25a1dadab300291a3;p=helm.git

diff --git a/helm/gTopLevel/reductionTactics.ml b/helm/gTopLevel/reductionTactics.ml
index 0080e4571..54b439b25 100644
--- a/helm/gTopLevel/reductionTactics.ml
+++ b/helm/gTopLevel/reductionTactics.ml
@@ -92,10 +92,10 @@ let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;;
 let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
 let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
 
-let fold_tac ~also_in_hypotheses ~term ~status:(proof,goal) =
+let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-  let term' = CicReduction.whd context term in
+  let term' = reduction context term in
    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
    (* the type of one metavariable. So we replace it everywhere.   *)
    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)