1. rewrite_* and rewrite_back_* merged into one function

[helm.git] / helm / ocaml / tactics / fourierR.ml

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index e6fa4edcd6275e92be398a3f358cf37a8fbcaba6..2fbba97ad5b7d905d48b8ddde2c96bf40a252136 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -886,7 +886,10 @@ let equality_replace a b =
     let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
  debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
     let (proof,goals) = apply_tactic 
-     (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ())
+     (EqualityTactics.rewrite_simpl_tac
+       ~direction:`LeftToRight
+       ~pattern:(ProofEngineTypes.conclusion_pattern None)
+       (C.Meta (fresh_meta,irl)))
      ((curi,metasenv',pbo,pty),goal)
     in
     let new_goals = fresh_meta::goals in