X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=b9db6f705777eb9ae7acb09bace47a5cc6b1857c;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;hp=dd2c42f1cceb001f90f1d625b985cdeb9465a23a;hpb=0318a75de15f587bcbdb838984e8e59c913ec85c;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index dd2c42f1c..b9db6f705 100644
--- 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
@@ -143,8 +143,9 @@ let rewrite_back_simpl_tac ?where ~term () =
   ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
 ;;
 
-let replace_tac ~what ~with_what =
- let replace_tac ~what ~with_what status =
+let replace_tac ~pattern ~with_what =
+(*
+ let replace_tac ~pattern ~with_what status =
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -179,6 +180,7 @@ let replace_tac ~what ~with_what =
       raise (ProofEngineTypes.Fail "Replace: empty context")
  in
    ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
+*) assert false
 ;;