From 12f52743d6334941294b857016de05942e89a584 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 31 Jan 2006 10:59:09 +0000
Subject: [PATCH] Bug fixed: metasenv used in place of metasenv' during
 rewriting in an hypothesis.

---
 helm/ocaml/tactics/equalityTactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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]
-- 
2.39.2