]> matita.cs.unibo.it Git - helm.git/commitdiff
karma: every term the rewrite acts on must be substututed
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 28 Jun 2006 14:39:58 +0000 (14:39 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 28 Jun 2006 14:39:58 +0000 (14:39 +0000)
components/tactics/equalityTactics.ml

index 29f0574794b649704f87959c4505f4c22b755b35..69466c272a458ad4c49386ae69b5dad8895ed13a 100644 (file)
@@ -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