All exported names are now qualified. This avoids the need for "open" statements.

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

diff --git a/components/tactics/.depend b/components/tactics/.depend
index b52cdc6b3b99776b086fd07a406966bf3b87df3e..964011bfd1609a0355170ca53b1024c22970af70 100644 (file)
--- a/components/tactics/.depend
+++ b/components/tactics/.depend
@@ -63,8 +63,6 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     hashtbl_equiv.cmi metadataQuery.cmi 
 metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     hashtbl_equiv.cmx metadataQuery.cmi 
-closeCoercionGraph.cmo: closeCoercionGraph.cmi 
-closeCoercionGraph.cmx: closeCoercionGraph.cmi 
 universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi 
 universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi 
 autoTypes.cmo: autoTypes.cmi 
@@ -73,6 +71,8 @@ autoCache.cmo: universe.cmi autoCache.cmi
 autoCache.cmx: universe.cmx autoCache.cmi 
 paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi 
 paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi 
+closeCoercionGraph.cmo: closeCoercionGraph.cmi 
+closeCoercionGraph.cmx: closeCoercionGraph.cmi 
 paramodulation/subst.cmo: paramodulation/subst.cmi 
 paramodulation/subst.cmx: paramodulation/subst.cmi 
 paramodulation/equality.cmo: paramodulation/utils.cmi \
@@ -211,7 +211,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \
     introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
     compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi 
-declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
-declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
     declarative.cmi