X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FfourierR.ml;h=1123b506fcf9d4a3638b5152c89eebe3d2383f23;hb=4480f2625fce077f7389dde595920d25748820eb;hp=8b910bded8ebabe6c5695016930b4ef4325c721b;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/fourierR.ml b/components/tactics/fourierR.ml
index 8b910bded..1123b506f 100644
--- a/components/tactics/fourierR.ml
+++ b/components/tactics/fourierR.ml
@@ -885,7 +885,7 @@ let equality_replace a b =
      (EqualityTactics.rewrite_simpl_tac
        ~direction:`LeftToRight
        ~pattern:(ProofEngineTypes.conclusion_pattern None)
-       (C.Meta (fresh_meta,irl)))
+       (C.Meta (fresh_meta,irl)) [])
      ((curi,metasenv',pbo,pty),goal)
     in
     let new_goals = fresh_meta::goals in