First experimental version of the declarative proof language for Matita.

[helm.git] / components / tactics / .depend

diff --git a/components/tactics/.depend b/components/tactics/.depend
index 50083802753f2ac184c1e13d11d1a24ff04aa729..43ed94aa9dd287dcc9f31eed229e25d8ff636aed 100644 (file)
--- 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,5 @@ 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 declarative.cmi 
+declarative.cmx: tactics.cmx tacticals.cmx declarative.cmi