X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2F.depend.opt;h=a278f6f0836f66a12becb40648662f44c709a1e6;hb=9b09890767aaa93e512324f8e7f13e2cdeebac88;hp=94235e520de502017011d6b6de79c2674f319b5a;hpb=04f22df647f35080b499b720bca7bc0eb1794c64;p=helm.git

diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt
index 94235e520..a278f6f08 100644
--- a/helm/software/components/tactics/.depend.opt
+++ b/helm/software/components/tactics/.depend.opt
@@ -91,11 +91,11 @@ paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
 paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
     paramodulation/equality.cmx paramodulation/equality_indexing.cmi 
 paramodulation/indexing.cmo: paramodulation/utils.cmi \
-    paramodulation/subst.cmi paramodulation/founif.cmi \
+    paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/founif.cmi \
     paramodulation/equality_indexing.cmi paramodulation/equality.cmi \
     paramodulation/indexing.cmi 
 paramodulation/indexing.cmx: paramodulation/utils.cmx \
-    paramodulation/subst.cmx paramodulation/founif.cmx \
+    paramodulation/subst.cmx proofEngineTypes.cmx paramodulation/founif.cmx \
     paramodulation/equality_indexing.cmx paramodulation/equality.cmx \
     paramodulation/indexing.cmi 
 paramodulation/saturation.cmo: paramodulation/utils.cmi \