X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=66e895119daf37b7239ef88b48f46dad0d9ad6da;hb=1dd5176f6d6a6247ebf941a1f6319a909f43d5fc;hp=bdba623190cc8ab47fa6b533f232ff5a26aec7a7;hpb=251e2f428031db12bae815fb56862e3b6384f0f8;p=helm.git

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index bdba62319..66e895119 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -80,7 +80,10 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
 
 
 let rewrite_simpl_tac ~term ~status =
- Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:ReductionTactics.simpl_tac ~status
+ Tacticals.then_ ~start:(rewrite_tac ~term)
+  ~continuation:
+   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+  ~status
 ;;
 
 (******************** THE FOURIER TACTIC ***********************)
@@ -714,7 +717,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 ;