Huge reorganization of matita and ocaml.

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

diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli
index 895a799dceb871e74ae5230871b2e110f8d62317..1d60ae149676d23c129e64a043026d746b1c2d90 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.mli
+++ b/helm/ocaml/tactics/equalityTactics.mli
@@ -33,7 +33,7 @@ val rewrite_simpl_tac:
   
 val replace_tac: 
   pattern:ProofEngineTypes.lazy_pattern ->
-  with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
+  with_what:Cic.lazy_term -> ProofEngineTypes.tactic
 
 val reflexivity_tac: ProofEngineTypes.tactic
 val symmetry_tac: ProofEngineTypes.tactic