From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 13:17:30 +0000 (+0000)
Subject: Bug fixed: a wrong lift made select unuseful when wanted was an open term.
X-Git-Tag: PRE_GETTER_STORAGE~92
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7da6adde34e87f3ed5cf7a83215955c45ed7ea5a;p=helm.git

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 eb92f1351..aefb1c1e6 100644
--- 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'