added support for goal patterns

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

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 3556a85f2e43e47cf2370cc324b0d89121cd26d2..2ee088edbaf551c19239c51a2aab496a6b1dc8c4 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -885,7 +885,7 @@ 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 ~term:(C.Meta (fresh_meta,irl)) ())
      ((curi,metasenv',pbo,pty),goal)
     in
     let new_goals = fresh_meta::goals in