X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2F.depend.opt;h=d9d6034a11e090bef20f2d14ccd1d8fb4e5692e2;hb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8;hp=f48d55ea2535a0d243aaa7846a475aee41ed0a3d;hpb=1652681b5eb49332f1c78e6c26d3ae5c7253d382;p=helm.git

diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt
index f48d55ea2..d9d6034a1 100644
--- a/helm/software/components/tactics/.depend.opt
+++ b/helm/software/components/tactics/.depend.opt
@@ -1,11 +1,19 @@
+proofEngineTypes.cmi: 
 proofEngineHelpers.cmi: proofEngineTypes.cmi 
+proofEngineReduction.cmi: 
 continuationals.cmi: proofEngineTypes.cmi 
 tacticals.cmi: proofEngineTypes.cmi 
 reductionTactics.cmi: proofEngineTypes.cmi 
 proofEngineStructuralRules.cmi: proofEngineTypes.cmi 
 primitiveTactics.cmi: proofEngineTypes.cmi 
+hashtbl_equiv.cmi: 
 metadataQuery.cmi: proofEngineTypes.cmi 
+universe.cmi: 
 autoTypes.cmi: proofEngineTypes.cmi 
+autoCache.cmi: 
+paramodulation/utils.cmi: 
+closeCoercionGraph.cmi: 
+paramodulation/subst.cmi: 
 paramodulation/equality.cmi: paramodulation/utils.cmi \
     paramodulation/subst.cmi 
 paramodulation/founif.cmi: paramodulation/subst.cmi 
@@ -27,10 +35,13 @@ equalityTactics.cmi: proofEngineTypes.cmi
 auto.cmi: proofEngineTypes.cmi automationCache.cmi 
 destructTactic.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
+inversion_principle.cmi: 
 ring.cmi: proofEngineTypes.cmi 
 setoids.cmi: proofEngineTypes.cmi 
+fourier.cmi: 
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
+history.cmi: 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
 tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi 
 declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi 
@@ -176,10 +187,10 @@ ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \
     primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi 
 ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \
     primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi 
-setoids.cmo: proofEngineTypes.cmi primitiveTactics.cmi equalityTactics.cmi \
-    setoids.cmi 
-setoids.cmx: proofEngineTypes.cmx primitiveTactics.cmx equalityTactics.cmx \
-    setoids.cmi 
+setoids.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+    primitiveTactics.cmi equalityTactics.cmi setoids.cmi 
+setoids.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+    primitiveTactics.cmx equalityTactics.cmx setoids.cmi 
 fourier.cmo: fourier.cmi 
 fourier.cmx: fourier.cmi 
 fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \