removed deadcode / fixed typos (thanks to ocaml 3.09)

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index fd336910ea4a899e3d5fcdc15870bffd929afb12..a5541ab03d4d39265dbd25b79880c6b17900d7aa 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -301,7 +301,6 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
     List.concat (map2 "wrong number of arguments in application"
       (fun t1 t2 -> aux context t1 t2) terms1 terms2)
   in
-   let context_len = List.length context in
    let roots = aux context where term in
     match wanted with
        None -> [],metasenv,ugraph,roots
@@ -482,7 +481,6 @@ exception Fail of string Lazy.t
    let subst,metasenv,ugraph,ty_terms =
     select_in_term ~metasenv ~context ~ugraph ~term:ty
      ~pattern:(what,goal_pattern) in
-   let context_len = List.length context in
    let subst,metasenv,ugraph,context_terms =
     let subst,metasenv,ugraph,res,_ =
      (List.fold_right