- tactics:

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

diff --git a/components/tactics/fourierR.ml b/components/tactics/fourierR.ml
index 8b910bded8ebabe6c5695016930b4ef4325c721b..1123b506fcf9d4a3638b5152c89eebe3d2383f23 100644 (file)
--- 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