- big interface changes: open goals are now collected in a notebook

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 62e5d0f9ae016dd2ecacef01d115fdd3f41a128b..66e895119daf37b7239ef88b48f46dad0d9ad6da 100644 (file)
--- 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 ***********************)