1) moved select and pattern_of from cicUtil to proofEngineHelpers

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index dd2c42f1cceb001f90f1d625b985cdeb9465a23a..8cbfed96b9a9b13aef53f70ee58089be41554df7 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -66,11 +66,11 @@ let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
         match goal_path with
         | None -> assert false (* (==), [t1'] *)
         | Some path -> 
-            let roots = CicUtil.select ~term:gty' ~context:path in
+            let roots = ProofEngineHelpers.select ~term:gty' ~pattern:path in
             let subterms = 
               List.fold_left (
                 fun acc (i, r) -> 
-                  let wanted = CicSubstitution.lift i t1' in
+                  let wanted = CicSubstitution.lift (List.length i) t1' in
                   PEH.find_subterms ~eq:PER.alpha_equivalence ~wanted r @ acc
             ) [] roots
             in