From: Claudio Sacerdoti Coen 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: 0.4.95@7852~1647 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=979d6b24af322d882c104b53bd0a7fd5919287da;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/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