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 ***********************)
(*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 ;