A few other tactics made available to matita.

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 8cbfed96b9a9b13aef53f70ee58089be41554df7..b9db6f705777eb9ae7acb09bace47a5cc6b1857c 100644 (file)
--- 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
 ;;