added support for goal patterns

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

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index 7d57a0c1145190c4e24b74488f22326ee96bb755..698b34e9c9edc79c3b2e246f5668e3ad350d376f 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -23,11 +23,21 @@
  * 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: 
+  ?where:ProofEngineTypes.pattern -> 
+  term:Cic.term -> unit -> 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
+  
+val replace_tac: 
+  what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
 
 val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic