X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2F.depend;h=2ed8b5147261eaf8a07373e496682e87789d5791;hb=58fa214788e29e3eef8a66f9d2c0b7cdaed81aa9;hp=50083802753f2ac184c1e13d11d1a24ff04aa729;hpb=aa576f13a6fd64586b389880dec3e47f703cd300;p=helm.git

diff --git a/components/tactics/.depend b/components/tactics/.depend
index 500838027..2ed8b5147 100644
--- a/components/tactics/.depend
+++ b/components/tactics/.depend
@@ -24,10 +24,12 @@ autoTactic.cmi: proofEngineTypes.cmi
 discriminationTactics.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
 ring.cmi: proofEngineTypes.cmi 
+setoids.cmi: proofEngineTypes.cmi 
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
 tactics.cmi: proofEngineTypes.cmi 
+declarative.cmi: proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
 proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
@@ -63,17 +65,19 @@ paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi
 paramodulation/subst.cmo: paramodulation/subst.cmi 
 paramodulation/subst.cmx: paramodulation/subst.cmi 
 paramodulation/equality.cmo: paramodulation/utils.cmi \
-    paramodulation/subst.cmi proofEngineReduction.cmi \
+    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
     paramodulation/equality.cmi 
 paramodulation/equality.cmx: paramodulation/utils.cmx \
-    paramodulation/subst.cmx proofEngineReduction.cmx \
+    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
     paramodulation/equality.cmi 
 paramodulation/inference.cmo: paramodulation/utils.cmi \
-    paramodulation/subst.cmi proofEngineHelpers.cmi metadataQuery.cmi \
-    paramodulation/equality.cmi paramodulation/inference.cmi 
+    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
+    metadataQuery.cmi paramodulation/equality.cmi \
+    paramodulation/inference.cmi 
 paramodulation/inference.cmx: paramodulation/utils.cmx \
-    paramodulation/subst.cmx proofEngineHelpers.cmx metadataQuery.cmx \
-    paramodulation/equality.cmx paramodulation/inference.cmi 
+    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
+    metadataQuery.cmx paramodulation/equality.cmx \
+    paramodulation/inference.cmi 
 paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
     paramodulation/equality.cmi paramodulation/equality_indexing.cmi 
 paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
@@ -186,3 +190,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx paramodulation/saturation.cmx \
     introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
     autoTactic.cmx tactics.cmi 
+declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+    declarative.cmi 
+declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+    declarative.cmi