1. rewrite_* and rewrite_back_* merged into one function

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

diff --git a/helm/ocaml/tactics/tactics.ml b/helm/ocaml/tactics/tactics.ml
index fc2c1c75dc39e7e4d54cd1e188183d95b4270042..055c00528139b5defa52843582d2e7b1a8d5dbec 100644 (file)
--- a/helm/ocaml/tactics/tactics.ml
+++ b/helm/ocaml/tactics/tactics.ml
@@ -58,8 +58,6 @@ let reduce = ReductionTactics.reduce_tac
 let reflexivity = EqualityTactics.reflexivity_tac
 let replace = EqualityTactics.replace_tac
 let rewrite = EqualityTactics.rewrite_tac
-let rewrite_back = EqualityTactics.rewrite_back_tac
-let rewrite_back_simpl = EqualityTactics.rewrite_back_simpl_tac
 let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
 let right = IntroductionTactics.right_tac
 let ring = Ring.ring_tac