1. rewrite_* and rewrite_back_* merged into one function

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

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index a8730287e732fabd7b792a86a69a27940179578c..f78624c979849da21ae4b9f95c4769d1c67b0918 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -59,17 +59,11 @@ val replace :
   pattern:ProofEngineTypes.pattern ->
   with_what:Cic.term -> ProofEngineTypes.tactic
 val rewrite :
-  ?where:ProofEngineTypes.pattern ->
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back :
-  ?where:ProofEngineTypes.pattern ->
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_simpl :
-  ?where:ProofEngineTypes.pattern ->
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[ `LeftToRight | `RightToLeft ] ->
+  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
 val rewrite_simpl :
-  ?where:ProofEngineTypes.pattern ->
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[ `LeftToRight | `RightToLeft ] ->
+  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
 val right : ProofEngineTypes.tactic
 val ring : ProofEngineTypes.tactic
 val set_goal : int -> ProofEngineTypes.tactic