From 5929e58cedcbdc70ce429aae939219ce7555d953 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Jun 2006 14:39:58 +0000 Subject: [PATCH] karma: every term the rewrite acts on must be substututed --- helm/software/components/tactics/equalityTactics.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 29f057479..69466c272 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -146,6 +146,8 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit 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 pbo = CicMetaSubst.apply_subst subst pbo in + let pty = CicMetaSubst.apply_subst subst pty in let equality = CicMetaSubst.apply_subst subst equality in let abstr_gty = ProofEngineReduction.replace_lifting_csc 0 -- 2.39.2