A few other tactics made available to matita.

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

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index 698b34e9c9edc79c3b2e246f5668e3ad350d376f..d156ae440d0199940fa8f8b0d47e849c8f74e759 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -37,7 +37,8 @@ val rewrite_back_simpl_tac:
   term:Cic.term -> unit -> 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