removed deadcode / fixed typos (thanks to ocaml 3.09)

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 7ed946170b5e36e018304c7062a033f96a4cb20c..a8e32886371030ea1bc9fe13a567108fcd139019 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -35,7 +35,7 @@ let rec rewrite_tac ~direction ~pattern equality =
   assert (wanted = None);   (* this should be checked syntactically *)
   let proof,goal = status in
   let curi, metasenv, pbo, pty = proof in
-  let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
+  let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
   match hyps_pat with
      he::(_::_ as tl) ->
        PET.apply_tactic