1. rewrite_* and rewrite_back_* merged into one function

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

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index d156ae440d0199940fa8f8b0d47e849c8f74e759..a9b4d1d0b39ed0f7d876005a3b1441d8ffcee030 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -24,17 +24,11 @@
  *)
 
 val rewrite_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[`LeftToRight | `RightToLeft] ->
+  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
 val rewrite_simpl_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
-val rewrite_back_simpl_tac: 
-  ?where:ProofEngineTypes.pattern -> 
-  term:Cic.term -> unit -> ProofEngineTypes.tactic
+  direction:[`LeftToRight | `RightToLeft] ->
+  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
   
 val replace_tac: 
   pattern:ProofEngineTypes.pattern ->