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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 8cbfed96b..b9db6f705 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -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
 ;;