Bug fixed: metasenv used in place of metasenv' during rewriting in an

hypothesis.

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index b3dc1bb9e8f2788c3b2e849f1301aaf7da0c07f6..da7f599a9ec2b642291173c3d0c6c1d4a6fc5bf6 100644 (file)
--- 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]