- Unified : some definitions of unified \lambda\delta

[helm.git] / helm / software / components / tactics / equalityTactics.ml

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index 29f0574794b649704f87959c4505f4c22b755b35..1ef330bd230d0ef57122d80954efda2f0f56b518 100644 (file)
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -44,14 +44,16 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
         (Tacticals.then_
           (rewrite_tac ~direction
            ~pattern:(None,[he],None) equality)
-          (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality)
+          (rewrite_tac ~direction ~pattern:(None,tl,concl_pat)
+            (CicSubstitution.lift 1 equality))
         ) status
    | [_] as hyps_pat when concl_pat <> None ->
        PET.apply_tactic
         (Tacticals.then_
           (rewrite_tac ~direction
            ~pattern:(None,hyps_pat,None) equality)
-          (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality)
+          (rewrite_tac ~direction ~pattern:(None,[],concl_pat)
+            (CicSubstitution.lift 1 equality))
         ) status
    | _ ->
   let arg,dir2,tac,concl_pat,gty =
@@ -146,6 +148,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