X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FequalityTactics.ml;h=cca2c1a5902b9256736dd8b1001abe42c1d3ea22;hb=f340ae8d0be1c480c6a496a11157a6ccfb367c13;hp=da7f599a9ec2b642291173c3d0c6c1d4a6fc5bf6;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml
index da7f599a9..cca2c1a59 100644
--- a/components/tactics/equalityTactics.ml
+++ b/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