Bug fixed: a wrong lift made select unuseful when wanted was an open term.

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index eb92f13515f745566d9a23deff2052b8b8c94797..aefb1c1e6ee2f9cc265e99dcb719cc39b37ecf94 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -235,6 +235,7 @@ let select_in_term ~context ~term ~pattern:(wanted,where) =
   and auxs context terms1 terms2 =  (* as aux for list of terms *)
     List.concat (List.map2 (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 -> roots
@@ -242,10 +243,13 @@ let select_in_term ~context ~term ~pattern:(wanted,where) =
         let rec find_in_roots =
          function
             [] -> []
-          | (context,where)::tl ->
+          | (context',where)::tl ->
              let tl' = find_in_roots tl in
+             let context'_len = List.length context' in
              let found =
-              let wanted = CicSubstitution.lift (List.length context) wanted in
+              let wanted =
+               CicSubstitution.lift (context'_len - context_len) wanted
+              in
                find_subterms ~wanted ~context where
              in
               found @ tl'