* fold_tac has now a new parameter, which is the reduction to ``undo''

[helm.git] / helm / gTopLevel / fourierR.ml

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index c08183bebf889300aa8c56893930d4a842e3deaf..9076ae70fffce795573bb6733e8140a60e73da04 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -775,7 +775,8 @@ let r =
      (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
      Tacticals.then_
       ~start:
-        (ReductionTactics.fold_tac ~also_in_hypotheses:false
+        (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+          ~also_in_hypotheses:false
           ~term:
             (Cic.Appl
               [_Rle ; _R0 ;