X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=b3dc1bb9e8f2788c3b2e849f1301aaf7da0c07f6;hb=f17da39739c49297bf435896c8cb4e3ac83b95a6;hp=8304d7bb19264738127e76f6409988d69ab14934;hpb=e5cf3788ff8a5416ac13f9d33555ff6f46d89548;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 8304d7bb1..b3dc1bb9e 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -67,14 +67,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
         | _::tl -> find_hyp (n+1) tl
       in
        let arg,gty = find_hyp 1 context in
-       let last_hyp_name_of_status (proof,goal) =
-        let curi, metasenv, pbo, pty = proof in
-        let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-         match context with
-            (Some (Cic.Name s,_))::_ -> s
-          | _ -> assert false
-       in
-        let dummy = "dummy" in
+       let dummy = "dummy" in
         Some arg,false,
          (fun ~term typ ->
            Tacticals.seq