various updates, removed proofs for now because they are the real bottleneck!!

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index dd2c42f1cceb001f90f1d625b985cdeb9465a23a..b9db6f705777eb9ae7acb09bace47a5cc6b1857c 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
@@ -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
 ;;