X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.mli;h=b9112deed25c0f90da430502ec168f504a367782;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a9b4d1d0b39ed0f7d876005a3b1441d8ffcee030;hpb=2b01133527077e8dd554f0fbcc51368903dd3b8c;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index a9b4d1d0b..b9112deed 100644
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -32,7 +32,7 @@ val rewrite_simpl_tac:
   
 val replace_tac: 
   pattern:ProofEngineTypes.pattern ->
-  with_what:Cic.term -> ProofEngineTypes.tactic
+  with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
 
 val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic