X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.mli;h=a9b4d1d0b39ed0f7d876005a3b1441d8ffcee030;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=698b34e9c9edc79c3b2e246f5668e3ad350d376f;hpb=abd9e5cfa8e7b6923e0664a4813a0a842f5c4e76;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index 698b34e9c..a9b4d1d0b 100644
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -24,20 +24,15 @@
  *)
 
 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: 
-  what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
+  pattern:ProofEngineTypes.pattern ->
+  with_what:Cic.term -> ProofEngineTypes.tactic
 
 val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic