X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.mli;h=1d60ae149676d23c129e64a043026d746b1c2d90;hb=951069678fea0d6dcdde984320ec5057ddc57c3c;hp=b9112deed25c0f90da430502ec168f504a367782;hpb=d1126c6b78a3333bbf415daf027004496b77c2f4;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index b9112deed..1d60ae149 100644
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -25,14 +25,15 @@
 
 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 ->
-  with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
+  pattern:ProofEngineTypes.lazy_pattern ->
+  with_what:Cic.lazy_term -> ProofEngineTypes.tactic
 
 val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic