X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=cca2c1a5902b9256736dd8b1001abe42c1d3ea22;hb=15469f16ff6f86c6cc0107070775b6c03c0ec478;hp=da7f599a9ec2b642291173c3d0c6c1d4a6fc5bf6;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

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