X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=1ef330bd230d0ef57122d80954efda2f0f56b518;hb=0d1ecc789c6d57a3eef47a028634d316905ef317;hp=b1727fb7d401d35fa761a2dd9c4cbb3540c9bf6e;hpb=08a92d276c5477968b02f31097b6ed03185f34eb;p=helm.git

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index b1727fb7d..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 =
@@ -80,7 +82,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
                 ~pattern:
                   (None,[name,Cic.Implicit (Some `Hole)], None)
                 (ProofEngineTypes.const_lazy_term typ);
-               ProofEngineStructuralRules.clear dummy
+               ProofEngineStructuralRules.clear [dummy]
               ]),
          Some pat,gty
     | _::_ -> assert false
@@ -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
@@ -289,15 +293,15 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
                        (function ((proof,goal) as status) ->
                          let _,metasenv,_,_ = proof in
                          let _,context,_ = CicUtil.lookup_meta goal metasenv in
-                         let hyp =
+                         let hyps =
                           try
                            match List.hd context with
-                              Some (Cic.Name name,_) -> name
+                              Some (Cic.Name name,_) -> [name]
                             | _ -> assert false
                           with (Failure "hd") -> assert false
                          in
                           ProofEngineTypes.apply_tactic
-                           (ProofEngineStructuralRules.clear ~hyp) status))
+                           (ProofEngineStructuralRules.clear ~hyps) status))
                     ~continuation:(aux_tac (n + 1) tl));
               T.id_tac])
          status