X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FequalityTactics.mli;h=1d60ae149676d23c129e64a043026d746b1c2d90;hb=6355ac16ff3996e16d9d9cfb08e4184bc7962f8b;hp=7d57a0c1145190c4e24b74488f22326ee96bb755;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index 7d57a0c11..1d60ae149 100644
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -23,11 +23,17 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
-val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
+val rewrite_tac: 
+  direction:[`LeftToRight | `RightToLeft] ->
+  pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
+
+val rewrite_simpl_tac: 
+  direction:[`LeftToRight | `RightToLeft] ->
+  pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
+  
+val replace_tac: 
+  pattern:ProofEngineTypes.lazy_pattern ->
+  with_what:Cic.lazy_term -> ProofEngineTypes.tactic
 
 val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic