changed pattern datatype:

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

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index b9112deed25c0f90da430502ec168f504a367782..895a799dceb871e74ae5230871b2e110f8d62317 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -25,13 +25,14 @@
 
 val rewrite_tac: 
   direction:[`LeftToRight | `RightToLeft] ->
-  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
+  pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
+
 val rewrite_simpl_tac: 
   direction:[`LeftToRight | `RightToLeft] ->
-  pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
+  pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
   
 val replace_tac: 
-  pattern:ProofEngineTypes.pattern ->
+  pattern:ProofEngineTypes.lazy_pattern ->
   with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
 
 val reflexivity_tac: ProofEngineTypes.tactic