From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 19 Jul 2006 16:29:06 +0000 (+0000)
Subject: Bug fixed in rewrite in multiple hypothesis and/or conclusion: a lifting was
X-Git-Tag: make_still_working~7039
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71a810d2c99d13d27aac943771d75460294bf71f;p=helm.git

Bug fixed in rewrite in multiple hypothesis and/or conclusion: a lifting was
missing, as usual :-)
---

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index 69466c272..1ef330bd2 100644
--- 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 =