Dead code removed.

[helm.git] / helm / ocaml / tactics / equalityTactics.ml

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 8304d7bb19264738127e76f6409988d69ab14934..b3dc1bb9e8f2788c3b2e849f1301aaf7da0c07f6 100644 (file)
--- 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