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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 62e5d0f9a..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 ***********************)