Two bugs fixed in the apply tactic:

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 94cb0624bacd7911e184631750ef5fb97b7bc3a4..c56d3de2d75af9c4566d19a98ff568104c4d4699 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -47,7 +47,7 @@ let rewrite_tac ~direction ~pattern equality =
       CicUniv.empty_ugraph in 
   let (ty_eq,metasenv',arguments,fresh_meta) =
    ProofEngineHelpers.saturate_term
-    (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq in
+    (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in
   let equality =
    if List.length arguments = 0 then
     equality