From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 20 Feb 2006 14:47:00 +0000 (+0000)
Subject: Bug fixed: rewrite > t where t had occurrences of metavariables in it could
X-Git-Tag: make_still_working~7549
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=3cc1aec78e4c51aa766127487f19a3d38a4b56ae;p=helm.git

Bug fixed: rewrite > t where t had occurrences of metavariables in it could
fail because of a missing apply_subst.
---

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index da7f599a9..cca2c1a59 100644
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -145,6 +145,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
     selected_terms_with_context ([],[]) in
   let t1 = CicMetaSubst.apply_subst subst t1 in
   let t2 = CicMetaSubst.apply_subst subst t2 in
+  let ty = CicMetaSubst.apply_subst subst ty in
   let equality = CicMetaSubst.apply_subst subst equality in
   let abstr_gty =
    ProofEngineReduction.replace_lifting_csc 0