From 3cc1aec78e4c51aa766127487f19a3d38a4b56ae 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. --- helm/software/components/tactics/equalityTactics.ml | 1 + 1 file changed, 1 insertion(+) 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 -- 2.39.2