From 979d6b24af322d882c104b53bd0a7fd5919287da Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Feb 2006 14:47:00 +0000 Subject: [PATCH] Bug fixed: rewrite > t where t had occurrences of metavariables in it could fail because of a missing apply_subst. --- components/tactics/equalityTactics.ml | 1 + 1 file changed, 1 insertion(+) 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 -- 2.39.2