The fold tactic of proofEngine now uses ReductionTactics.fold_tac.

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

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