X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=da7f599a9ec2b642291173c3d0c6c1d4a6fc5bf6;hb=ac595177011c8fd73c39fb9b5aaf8b130fb03ef3;hp=b3dc1bb9e8f2788c3b2e849f1301aaf7da0c07f6;hpb=f17da39739c49297bf435896c8cb4e3ac83b95a6;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index b3dc1bb9e..da7f599a9 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -163,7 +163,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
         metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
     | Some arg ->
        let gty' = CicSubstitution.subst t1 abstr_gty in
-        metasenv,arg,gty'
+        metasenv',arg,gty'
   in
   let exact_proof = 
     C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality]