X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fauto.ml;h=65087f8cbd14571035e856d22ecf389254098714;hb=3f586b01da59fe16b3d7f37da28bdd71f2225131;hp=5f110bc4c39030d22f6f051525c097ba00391fa0;hpb=172588c02ff4d9ed5cc03265c2bd6a36f8a0f5da;p=helm.git

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 5f110bc4c..65087f8cb 100644
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -452,7 +452,7 @@ let new_metasenv_and_unify_and_t
   ProofEngineTypes.apply_tactic
     (EqualityTactics.rewrite_tac ~direction:`RightToLeft
       ~pattern:(ProofEngineTypes.conclusion_pattern None) 
-        (Cic.Meta(newmeta,irl)))
+        (Cic.Meta(newmeta,irl)) [])
    (proof'',goal)
  in
  let goal = match goals with [g] -> g | _ -> assert false in