now we try two distinct depend files for compilation in byte and native code

diff --git a/helm/software/components/Makefile.common b/helm/software/components/Makefile.common
index b6ad6eb963c4b7a1f6775a0d1d9204f580977d5c..30bd4c8898b29c533655d94ddc5553ed9d908624 100644 (file)
--- a/helm/software/components/Makefile.common
+++ b/helm/software/components/Makefile.common
@@ -7,7 +7,7 @@ H=@
 #  $IMPLEMENTATION_FILES
 #  $EXTRA_OBJECTS_TO_INSTALL
 #  $EXTRA_OBJECTS_TO_CLEAN
-# and put in a directory where there is a .depend file.
+# and put in a directory where there is a .depend or .depend.opt file.
 
 # $OCAMLFIND must be set to a meaningful vaule, including OCAMLPATH=
 
@@ -75,11 +75,12 @@ depend:: $(DEPEND_FILES)
 depend.opt:: $(DEPEND_FILES)
        $(H)echo "  OCAMLDEP -native"
        $(H)$(OCAMLDEP) -native \
-               $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend
+               $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend.opt
 
 $(PACKAGE).ps: .dep.dot
        dot -Tps -o $@ $<
 
+# FG: .depend or .depend.opt? 
 .dep.dot: .depend
        ocamldot < .depend > $@
 
@@ -129,13 +130,18 @@ STATS_FILES = \
        echo -n "LOC:" >> .stats
        wc -l $(STATS_FILES) | tail -1 | awk '{ print $$1 }' >> .stats
 
-.PHONY: all opt world backup depend install uninstall clean ocamlinit
+.PHONY: all opt backup depend depend.opt install uninstall clean ocamlinit
 
-ifneq ($(MAKECMDGOALS), depend)
- ifneq ($(MAKECMDGOALS), depend.opt)
-   include .depend   
- endif
+ifeq ($(MAKECMDGOALS),)
+  include .depend   
 endif
 
-NULL =
+ifeq ($(MAKECMDGOALS), all)
+  include .depend   
+endif
 
+ifeq ($(MAKECMDGOALS), opt)
+  include .depend.opt   
+endif
+
+NULL =

diff --git a/helm/software/components/acic_content/.depend.opt b/helm/software/components/acic_content/.depend.opt
new file mode 100644 (file)
index 0000000..fef8792
--- /dev/null
+++ b/helm/software/components/acic_content/.depend.opt
@@ -0,0 +1,27 @@
+acic2content.cmi: content.cmi 
+content2cic.cmi: content.cmi 
+cicNotationUtil.cmi: cicNotationPt.cmx 
+cicNotationEnv.cmi: cicNotationPt.cmx 
+cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi 
+acic2astMatcher.cmi: cicNotationPt.cmx 
+termAcicContent.cmi: cicNotationPt.cmx 
+content.cmo: content.cmi 
+content.cmx: content.cmi 
+acic2content.cmo: content.cmi acic2content.cmi 
+acic2content.cmx: content.cmx acic2content.cmi 
+content2cic.cmo: content.cmi content2cic.cmi 
+content2cic.cmx: content.cmx content2cic.cmi 
+cicNotationUtil.cmo: cicNotationPt.cmx cicNotationUtil.cmi 
+cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi 
+cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmx cicNotationEnv.cmi 
+cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi 
+cicNotationPp.cmo: cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmi 
+cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi 
+acic2astMatcher.cmo: cicNotationUtil.cmi cicNotationPt.cmx cicNotationPp.cmi \
+    acic2astMatcher.cmi 
+acic2astMatcher.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \
+    acic2astMatcher.cmi 
+termAcicContent.cmo: cicNotationUtil.cmi cicNotationPt.cmx cicNotationPp.cmi \
+    acic2content.cmi acic2astMatcher.cmi termAcicContent.cmi 
+termAcicContent.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \
+    acic2content.cmx acic2astMatcher.cmx termAcicContent.cmi 

diff --git a/helm/software/components/binaries/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/helm/software/components/binaries/extractor/Makefile b/helm/software/components/binaries/extractor/Makefile
index f7151e3cbabf8eb1a7e5a3031fa77b37d12c1e9a..eae5c635d52010e252db7f34695857af8b10eb77 100644 (file)
--- a/helm/software/components/binaries/extractor/Makefile
+++ b/helm/software/components/binaries/extractor/Makefile
@@ -38,7 +38,18 @@ depend:
        $(H)ocamldep extractor.ml extractor_manager.ml > .depend
 depend.opt: 
        $(H)echo "  OCAMLDEP -native"
-       $(H)ocamldep -native extractor.ml extractor_manager.ml > .depend
+       $(H)ocamldep -native extractor.ml extractor_manager.ml > .depend.opt
+
+ifeq ($(MAKECMDGOALS),)
+  include .depend   
+endif
+
+ifeq ($(MAKECMDGOALS), all)
+  include .depend   
+endif
+
+ifeq ($(MAKECMDGOALS), opt)
+  include .depend.opt   
+endif
 
-include .depend
 include ../../../Makefile.defs

diff --git a/helm/software/components/binaries/saturate/Makefile b/helm/software/components/binaries/saturate/Makefile
index 567e3b0d3e58abca88e0c89a8bb34a179888f317..ecd8d9111e0d868030413700112e4cfa334b2aaa 100644 (file)
--- a/helm/software/components/binaries/saturate/Makefile
+++ b/helm/software/components/binaries/saturate/Makefile
@@ -28,5 +28,6 @@ clean:
        $(H)rm -f saturate saturate.opt
 
 depend:
+depend.opt:
 
 include ../../../Makefile.defs

diff --git a/helm/software/components/binaries/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/helm/software/components/binaries/table_creator/Makefile b/helm/software/components/binaries/table_creator/Makefile
index 15cf1863aaf08ce65a1b61603061d4616790ddf7..23e732629abb8b329c1a3771b56cde6ec23f4309 100644 (file)
--- a/helm/software/components/binaries/table_creator/Makefile
+++ b/helm/software/components/binaries/table_creator/Makefile
@@ -39,7 +39,18 @@ depend:
        $(H)ocamldep table_creator.ml > .depend
 depend.opt: 
        $(H)echo "  OCAMLDEP -native"
-       $(H)ocamldep -native table_creator.ml > .depend
+       $(H)ocamldep -native table_creator.ml > .depend.opt
+
+ifeq ($(MAKECMDGOALS),)
+  include .depend   
+endif
+
+ifeq ($(MAKECMDGOALS), all)
+  include .depend   
+endif
+
+ifeq ($(MAKECMDGOALS), opt)
+  include .depend.opt   
+endif
 
-include .depend
 include ../../../Makefile.defs

diff --git a/helm/software/components/binaries/utilities/.depend.opt b/helm/software/components/binaries/utilities/.depend.opt
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/helm/software/components/binaries/utilities/Makefile b/helm/software/components/binaries/utilities/Makefile
index 314136db57dabda1d015fd7df4f030898d4c8e53..1874a238543eb464f05813e53a522c2366ec644f 100644 (file)
--- a/helm/software/components/binaries/utilities/Makefile
+++ b/helm/software/components/binaries/utilities/Makefile
@@ -23,7 +23,19 @@ depend:
        $(H)ocamldep extractor.ml extractor_manager.ml > .depend
 depend.opt: 
        $(H)echo "  OCAMLDEP -native"
-       $(H)ocamldep -native extractor.ml extractor_manager.ml > .depend
+       $(H)ocamldep -native extractor.ml extractor_manager.ml > .depend.opt
+       
+ifeq ($(MAKECMDGOALS),)
+  include .depend   
+endif
 
+ifeq ($(MAKECMDGOALS), all)
+  include .depend   
+endif
+
+ifeq ($(MAKECMDGOALS), opt)
+  include .depend.opt   
+endif
+       
 include ../../../Makefile.defs
 

diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt
new file mode 100644 (file)
index 0000000..44b016d
--- /dev/null
+++ b/helm/software/components/cic/.depend.opt
@@ -0,0 +1,27 @@
+unshare.cmi: cic.cmx 
+deannotate.cmi: cic.cmx 
+cicParser.cmi: cic.cmx 
+cicUtil.cmi: cic.cmx 
+helmLibraryObjects.cmi: cic.cmx 
+discrimination_tree.cmi: cic.cmx 
+path_indexing.cmi: cic.cmx 
+cic.cmo: cicUniv.cmi 
+cic.cmx: cicUniv.cmx 
+unshare.cmo: cic.cmx unshare.cmi 
+unshare.cmx: cic.cmx unshare.cmi 
+cicUniv.cmo: cicUniv.cmi 
+cicUniv.cmx: cicUniv.cmi 
+deannotate.cmo: cic.cmx deannotate.cmi 
+deannotate.cmx: cic.cmx deannotate.cmi 
+cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmx cicParser.cmi 
+cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi 
+cicUtil.cmo: cicUniv.cmi cic.cmx cicUtil.cmi 
+cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi 
+helmLibraryObjects.cmo: cic.cmx helmLibraryObjects.cmi 
+helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi 
+libraryObjects.cmo: libraryObjects.cmi 
+libraryObjects.cmx: libraryObjects.cmi 
+discrimination_tree.cmo: cicUtil.cmi cic.cmx discrimination_tree.cmi 
+discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi 
+path_indexing.cmo: cic.cmx path_indexing.cmi 
+path_indexing.cmx: cic.cmx path_indexing.cmi 

diff --git a/helm/software/components/cic_acic/.depend.opt b/helm/software/components/cic_acic/.depend.opt
new file mode 100644 (file)
index 0000000..3fc1e0d
--- /dev/null
+++ b/helm/software/components/cic_acic/.depend.opt
@@ -0,0 +1,9 @@
+cic2Xml.cmi: cic2acic.cmi 
+eta_fixing.cmo: eta_fixing.cmi 
+eta_fixing.cmx: eta_fixing.cmi 
+doubleTypeInference.cmo: doubleTypeInference.cmi 
+doubleTypeInference.cmx: doubleTypeInference.cmi 
+cic2acic.cmo: eta_fixing.cmi doubleTypeInference.cmi cic2acic.cmi 
+cic2acic.cmx: eta_fixing.cmx doubleTypeInference.cmx cic2acic.cmi 
+cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi 
+cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi 

diff --git a/helm/software/components/cic_disambiguation/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt
new file mode 100644 (file)
index 0000000..ca41244
--- /dev/null
+++ b/helm/software/components/cic_disambiguation/.depend.opt
@@ -0,0 +1,12 @@
+disambiguateChoices.cmi: disambiguateTypes.cmi 
+disambiguate.cmi: disambiguateTypes.cmi 
+disambiguateTypes.cmo: disambiguateTypes.cmi 
+disambiguateTypes.cmx: disambiguateTypes.cmi 
+disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi 
+disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi 
+disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \
+    disambiguate.cmi 
+disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
+    disambiguate.cmi 
+number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi 
+number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx 

diff --git a/helm/software/components/cic_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt
new file mode 100644 (file)
index 0000000..06b9188
--- /dev/null
+++ b/helm/software/components/cic_proof_checking/.depend.opt
@@ -0,0 +1,24 @@
+cicLogger.cmo: cicLogger.cmi 
+cicLogger.cmx: cicLogger.cmi 
+cicEnvironment.cmo: cicEnvironment.cmi 
+cicEnvironment.cmx: cicEnvironment.cmi 
+cicPp.cmo: cicEnvironment.cmi cicPp.cmi 
+cicPp.cmx: cicEnvironment.cmx cicPp.cmi 
+cicUnivUtils.cmo: cicEnvironment.cmi cicUnivUtils.cmi 
+cicUnivUtils.cmx: cicEnvironment.cmx cicUnivUtils.cmi 
+cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi 
+cicSubstitution.cmx: cicEnvironment.cmx cicSubstitution.cmi 
+cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi 
+cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi 
+cicReduction.cmo: cicSubstitution.cmi cicPp.cmi cicEnvironment.cmi \
+    cicReduction.cmi 
+cicReduction.cmx: cicSubstitution.cmx cicPp.cmx cicEnvironment.cmx \
+    cicReduction.cmi 
+cicTypeChecker.cmo: cicUnivUtils.cmi cicSubstitution.cmi cicReduction.cmi \
+    cicPp.cmi cicLogger.cmi cicEnvironment.cmi cicTypeChecker.cmi 
+cicTypeChecker.cmx: cicUnivUtils.cmx cicSubstitution.cmx cicReduction.cmx \
+    cicPp.cmx cicLogger.cmx cicEnvironment.cmx cicTypeChecker.cmi 
+freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \
+    freshNamesGenerator.cmi 
+freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \
+    freshNamesGenerator.cmi 

diff --git a/helm/software/components/cic_unification/.depend.opt b/helm/software/components/cic_unification/.depend.opt
new file mode 100644 (file)
index 0000000..9fa71a6
--- /dev/null
+++ b/helm/software/components/cic_unification/.depend.opt
@@ -0,0 +1,14 @@
+cicMetaSubst.cmo: cicMetaSubst.cmi 
+cicMetaSubst.cmx: cicMetaSubst.cmi 
+cicMkImplicit.cmo: cicMkImplicit.cmi 
+cicMkImplicit.cmx: cicMkImplicit.cmi 
+termUtil.cmo: cicMkImplicit.cmi termUtil.cmi 
+termUtil.cmx: cicMkImplicit.cmx termUtil.cmi 
+coercGraph.cmo: termUtil.cmi cicMkImplicit.cmi coercGraph.cmi 
+coercGraph.cmx: termUtil.cmx cicMkImplicit.cmx coercGraph.cmi 
+cicUnification.cmo: coercGraph.cmi cicMetaSubst.cmi cicUnification.cmi 
+cicUnification.cmx: coercGraph.cmx cicMetaSubst.cmx cicUnification.cmi 
+cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \
+    cicMetaSubst.cmi cicRefine.cmi 
+cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \
+    cicMetaSubst.cmx cicRefine.cmi 

diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend
index d2bd17f191ea5327dd22488ba428ef69c285f610..759898ac62d342cc27c7eedb2251fb840dbbc47d 100644 (file)
--- a/helm/software/components/content_pres/.depend
+++ b/helm/software/components/content_pres/.depend
@@ -34,10 +34,6 @@ cicClassify.cmo: cicClassify.cmi
 cicClassify.cmx: cicClassify.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
-content2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi \
-    content2Procedural.cmi 
-content2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx \
-    content2Procedural.cmi 
 acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi 
 acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi 
 objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \

diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt
new file mode 100644 (file)
index 0000000..759898a
--- /dev/null
+++ b/helm/software/components/content_pres/.depend.opt
@@ -0,0 +1,46 @@
+cicNotationPres.cmi: mpresentation.cmi box.cmi 
+boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi 
+content2pres.cmi: cicNotationPres.cmi 
+sequent2pres.cmi: cicNotationPres.cmi 
+renderingAttrs.cmo: renderingAttrs.cmi 
+renderingAttrs.cmx: renderingAttrs.cmi 
+cicNotationLexer.cmo: cicNotationLexer.cmi 
+cicNotationLexer.cmx: cicNotationLexer.cmi 
+cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi 
+cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi 
+mpresentation.cmo: mpresentation.cmi 
+mpresentation.cmx: mpresentation.cmi 
+box.cmo: renderingAttrs.cmi box.cmi 
+box.cmx: renderingAttrs.cmx box.cmi 
+content2presMatcher.cmo: content2presMatcher.cmi 
+content2presMatcher.cmx: content2presMatcher.cmi 
+termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \
+    termContentPres.cmi 
+termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \
+    termContentPres.cmi 
+cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
+    cicNotationPres.cmi 
+cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
+    cicNotationPres.cmi 
+boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
+    boxPp.cmi 
+boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
+    boxPp.cmi 
+content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
+    cicNotationPres.cmi box.cmi content2pres.cmi 
+content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
+    cicNotationPres.cmx box.cmx content2pres.cmi 
+cicClassify.cmo: cicClassify.cmi 
+cicClassify.cmx: cicClassify.cmi 
+proceduralTypes.cmo: proceduralTypes.cmi 
+proceduralTypes.cmx: proceduralTypes.cmi 
+acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi 
+acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi 
+objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \
+    acic2Procedural.cmi objPp.cmi 
+objPp.cmx: termContentPres.cmx content2pres.cmx cicNotationPres.cmx boxPp.cmx \
+    acic2Procedural.cmx objPp.cmi 
+sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \
+    box.cmi sequent2pres.cmi 
+sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \
+    box.cmx sequent2pres.cmi 

diff --git a/helm/software/components/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt
new file mode 100644 (file)
index 0000000..6d96e61
--- /dev/null
+++ b/helm/software/components/extlib/.depend.opt
@@ -0,0 +1,18 @@
+componentsConf.cmo: componentsConf.cmi 
+componentsConf.cmx: componentsConf.cmi 
+hExtlib.cmo: hExtlib.cmi 
+hExtlib.cmx: hExtlib.cmi 
+hMarshal.cmo: hExtlib.cmi hMarshal.cmi 
+hMarshal.cmx: hExtlib.cmx hMarshal.cmi 
+patternMatcher.cmo: patternMatcher.cmi 
+patternMatcher.cmx: patternMatcher.cmi 
+hLog.cmo: hLog.cmi 
+hLog.cmx: hLog.cmi 
+trie.cmo: trie.cmi 
+trie.cmx: trie.cmi 
+hTopoSort.cmo: hTopoSort.cmi 
+hTopoSort.cmx: hTopoSort.cmi 
+refCounter.cmo: refCounter.cmi 
+refCounter.cmx: refCounter.cmi 
+graphvizPp.cmo: graphvizPp.cmi 
+graphvizPp.cmx: graphvizPp.cmi 

diff --git a/helm/software/components/getter/.depend.opt b/helm/software/components/getter/.depend.opt
new file mode 100644 (file)
index 0000000..554fb1e
--- /dev/null
+++ b/helm/software/components/getter/.depend.opt
@@ -0,0 +1,31 @@
+http_getter_env.cmi: http_getter_types.cmx 
+http_getter_common.cmi: http_getter_types.cmx 
+http_getter.cmi: http_getter_types.cmx 
+http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi 
+http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi 
+http_getter_logger.cmo: http_getter_logger.cmi 
+http_getter_logger.cmx: http_getter_logger.cmi 
+http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi 
+http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi 
+http_getter_const.cmo: http_getter_const.cmi 
+http_getter_const.cmx: http_getter_const.cmi 
+http_getter_env.cmo: http_getter_types.cmx http_getter_misc.cmi \
+    http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi 
+http_getter_env.cmx: http_getter_types.cmx http_getter_misc.cmx \
+    http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi 
+http_getter_storage.cmo: http_getter_wget.cmi http_getter_types.cmx \
+    http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi 
+http_getter_storage.cmx: http_getter_wget.cmx http_getter_types.cmx \
+    http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi 
+http_getter_common.cmo: http_getter_types.cmx http_getter_misc.cmi \
+    http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi 
+http_getter_common.cmx: http_getter_types.cmx http_getter_misc.cmx \
+    http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi 
+http_getter.cmo: http_getter_wget.cmi http_getter_types.cmx \
+    http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \
+    http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \
+    http_getter.cmi 
+http_getter.cmx: http_getter_wget.cmx http_getter_types.cmx \
+    http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
+    http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
+    http_getter.cmi 

diff --git a/helm/software/components/grafite/.depend.opt b/helm/software/components/grafite/.depend.opt
new file mode 100644 (file)
index 0000000..0f64ba7
--- /dev/null
+++ b/helm/software/components/grafite/.depend.opt
@@ -0,0 +1,6 @@
+grafiteAstPp.cmi: grafiteAst.cmx 
+grafiteMarshal.cmi: grafiteAst.cmx 
+grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi 
+grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi 
+grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi 
+grafiteMarshal.cmx: grafiteAstPp.cmx grafiteAst.cmx grafiteMarshal.cmi 

diff --git a/helm/software/components/grafite_engine/.depend.opt b/helm/software/components/grafite_engine/.depend.opt
new file mode 100644 (file)
index 0000000..b0d4b70
--- /dev/null
+++ b/helm/software/components/grafite_engine/.depend.opt
@@ -0,0 +1,8 @@
+grafiteSync.cmi: grafiteTypes.cmi 
+grafiteEngine.cmi: grafiteTypes.cmi 
+grafiteTypes.cmo: grafiteTypes.cmi 
+grafiteTypes.cmx: grafiteTypes.cmi 
+grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi 
+grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi 
+grafiteEngine.cmo: grafiteTypes.cmi grafiteSync.cmi grafiteEngine.cmi 
+grafiteEngine.cmx: grafiteTypes.cmx grafiteSync.cmx grafiteEngine.cmi 

diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt
new file mode 100644 (file)
index 0000000..2dc8a7c
--- /dev/null
+++ b/helm/software/components/grafite_parser/.depend.opt
@@ -0,0 +1,13 @@
+grafiteWalker.cmi: grafiteParser.cmi 
+dependenciesParser.cmo: dependenciesParser.cmi 
+dependenciesParser.cmx: dependenciesParser.cmi 
+grafiteParser.cmo: dependenciesParser.cmi grafiteParser.cmi 
+grafiteParser.cmx: dependenciesParser.cmx grafiteParser.cmi 
+cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi 
+cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi 
+grafiteDisambiguator.cmo: grafiteDisambiguator.cmi 
+grafiteDisambiguator.cmx: grafiteDisambiguator.cmi 
+grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi 
+grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi 
+grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi 
+grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi 

diff --git a/helm/software/components/hgdome/.depend.opt b/helm/software/components/hgdome/.depend.opt
new file mode 100644 (file)
index 0000000..bf9c09a
--- /dev/null
+++ b/helm/software/components/hgdome/.depend.opt
@@ -0,0 +1,4 @@
+domMisc.cmo: domMisc.cmi 
+domMisc.cmx: domMisc.cmi 
+xml2Gdome.cmo: xml2Gdome.cmi 
+xml2Gdome.cmx: xml2Gdome.cmi 

diff --git a/helm/software/components/hmysql/.depend.opt b/helm/software/components/hmysql/.depend.opt
new file mode 100644 (file)
index 0000000..e67a066
--- /dev/null
+++ b/helm/software/components/hmysql/.depend.opt
@@ -0,0 +1,2 @@
+hMysql.cmo: hMysql.cmi 
+hMysql.cmx: hMysql.cmi 

diff --git a/helm/software/components/lexicon/.depend.opt b/helm/software/components/lexicon/.depend.opt
new file mode 100644 (file)
index 0000000..7fec1d3
--- /dev/null
+++ b/helm/software/components/lexicon/.depend.opt
@@ -0,0 +1,20 @@
+lexiconAstPp.cmi: lexiconAst.cmx 
+disambiguatePp.cmi: lexiconAst.cmx 
+lexiconMarshal.cmi: lexiconAst.cmx 
+cicNotation.cmi: lexiconAst.cmx 
+lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi 
+lexiconSync.cmi: lexiconEngine.cmi 
+lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi 
+lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi 
+disambiguatePp.cmo: lexiconAstPp.cmi lexiconAst.cmx disambiguatePp.cmi 
+disambiguatePp.cmx: lexiconAstPp.cmx lexiconAst.cmx disambiguatePp.cmi 
+lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi 
+lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi 
+cicNotation.cmo: lexiconAst.cmx cicNotation.cmi 
+cicNotation.cmx: lexiconAst.cmx cicNotation.cmi 
+lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmx disambiguatePp.cmi \
+    cicNotation.cmi lexiconEngine.cmi 
+lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx disambiguatePp.cmx \
+    cicNotation.cmx lexiconEngine.cmi 
+lexiconSync.cmo: lexiconEngine.cmi cicNotation.cmi lexiconSync.cmi 
+lexiconSync.cmx: lexiconEngine.cmx cicNotation.cmx lexiconSync.cmi 

diff --git a/helm/software/components/library/.depend.opt b/helm/software/components/library/.depend.opt
new file mode 100644 (file)
index 0000000..eacb269
--- /dev/null
+++ b/helm/software/components/library/.depend.opt
@@ -0,0 +1,24 @@
+cicCoercion.cmi: refinementTool.cmx coercDb.cmi 
+librarySync.cmi: refinementTool.cmx 
+cicElim.cmo: cicElim.cmi 
+cicElim.cmx: cicElim.cmi 
+cicRecord.cmo: cicRecord.cmi 
+cicRecord.cmx: cicRecord.cmi 
+libraryMisc.cmo: libraryMisc.cmi 
+libraryMisc.cmx: libraryMisc.cmi 
+libraryDb.cmo: libraryDb.cmi 
+libraryDb.cmx: libraryDb.cmi 
+coercDb.cmo: coercDb.cmi 
+coercDb.cmx: coercDb.cmi 
+cicCoercion.cmo: refinementTool.cmx coercDb.cmi cicCoercion.cmi 
+cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi 
+librarySync.cmo: refinementTool.cmx libraryDb.cmi coercDb.cmi cicRecord.cmi \
+    cicElim.cmi cicCoercion.cmi librarySync.cmi 
+librarySync.cmx: refinementTool.cmx libraryDb.cmx coercDb.cmx cicRecord.cmx \
+    cicElim.cmx cicCoercion.cmx librarySync.cmi 
+libraryNoDb.cmo: libraryNoDb.cmi 
+libraryNoDb.cmx: libraryNoDb.cmi 
+libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \
+    libraryDb.cmi libraryClean.cmi 
+libraryClean.cmx: librarySync.cmx libraryNoDb.cmx libraryMisc.cmx \
+    libraryDb.cmx libraryClean.cmi 

diff --git a/helm/software/components/logger/.depend.opt b/helm/software/components/logger/.depend.opt
new file mode 100644 (file)
index 0000000..28268d2
--- /dev/null
+++ b/helm/software/components/logger/.depend.opt
@@ -0,0 +1,2 @@
+helmLogger.cmo: helmLogger.cmi 
+helmLogger.cmx: helmLogger.cmi 

diff --git a/helm/software/components/metadata/.depend.opt b/helm/software/components/metadata/.depend.opt
new file mode 100644 (file)
index 0000000..492a34e
--- /dev/null
+++ b/helm/software/components/metadata/.depend.opt
@@ -0,0 +1,23 @@
+metadataExtractor.cmi: metadataTypes.cmi 
+metadataPp.cmi: metadataTypes.cmi 
+metadataConstraints.cmi: metadataTypes.cmi 
+metadataDb.cmi: metadataTypes.cmi 
+metadataDeps.cmi: metadataTypes.cmi 
+sqlStatements.cmo: sqlStatements.cmi 
+sqlStatements.cmx: sqlStatements.cmi 
+metadataTypes.cmo: metadataTypes.cmi 
+metadataTypes.cmx: metadataTypes.cmi 
+metadataExtractor.cmo: metadataTypes.cmi metadataExtractor.cmi 
+metadataExtractor.cmx: metadataTypes.cmx metadataExtractor.cmi 
+metadataPp.cmo: metadataTypes.cmi metadataPp.cmi 
+metadataPp.cmx: metadataTypes.cmx metadataPp.cmi 
+metadataConstraints.cmo: metadataTypes.cmi metadataPp.cmi \
+    metadataConstraints.cmi 
+metadataConstraints.cmx: metadataTypes.cmx metadataPp.cmx \
+    metadataConstraints.cmi 
+metadataDb.cmo: metadataTypes.cmi metadataPp.cmi metadataExtractor.cmi \
+    metadataConstraints.cmi metadataDb.cmi 
+metadataDb.cmx: metadataTypes.cmx metadataPp.cmx metadataExtractor.cmx \
+    metadataConstraints.cmx metadataDb.cmi 
+metadataDeps.cmo: sqlStatements.cmi metadataTypes.cmi metadataDeps.cmi 
+metadataDeps.cmx: sqlStatements.cmx metadataTypes.cmx metadataDeps.cmi 

diff --git a/helm/software/components/registry/.depend.opt b/helm/software/components/registry/.depend.opt
new file mode 100644 (file)
index 0000000..cf4f36b
--- /dev/null
+++ b/helm/software/components/registry/.depend.opt
@@ -0,0 +1,2 @@
+helm_registry.cmo: helm_registry.cmi 
+helm_registry.cmx: helm_registry.cmi 

diff --git a/helm/software/components/syntax_extensions/.depend.opt b/helm/software/components/syntax_extensions/.depend.opt
new file mode 100644 (file)
index 0000000..c0cd9c9
--- /dev/null
+++ b/helm/software/components/syntax_extensions/.depend.opt
@@ -0,0 +1,2 @@
+utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi 
+utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 

diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt
new file mode 100644 (file)
index 0000000..6c23fc9
--- /dev/null
+++ b/helm/software/components/tactics/.depend.opt
@@ -0,0 +1,210 @@
+proofEngineHelpers.cmi: proofEngineTypes.cmi 
+continuationals.cmi: proofEngineTypes.cmi 
+tacticals.cmi: proofEngineTypes.cmi continuationals.cmi 
+reductionTactics.cmi: proofEngineTypes.cmi 
+proofEngineStructuralRules.cmi: proofEngineTypes.cmi 
+primitiveTactics.cmi: proofEngineTypes.cmi 
+metadataQuery.cmi: proofEngineTypes.cmi 
+autoTypes.cmi: proofEngineTypes.cmi 
+paramodulation/equality.cmi: paramodulation/utils.cmi \
+    paramodulation/subst.cmi 
+paramodulation/founif.cmi: paramodulation/subst.cmi 
+paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \
+    paramodulation/equality.cmi 
+paramodulation/indexing.cmi: paramodulation/utils.cmi \
+    paramodulation/subst.cmi paramodulation/equality_indexing.cmi \
+    paramodulation/equality.cmi 
+paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
+    paramodulation/indexing.cmi paramodulation/equality.cmi 
+variousTactics.cmi: proofEngineTypes.cmi 
+introductionTactics.cmi: proofEngineTypes.cmi 
+eliminationTactics.cmi: proofEngineTypes.cmi 
+negationTactics.cmi: proofEngineTypes.cmi 
+equalityTactics.cmi: proofEngineTypes.cmi 
+auto.cmi: universe.cmi proofEngineTypes.cmi 
+autoTactic.cmi: universe.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: universe.cmi proofEngineTypes.cmi 
+declarative.cmi: universe.cmi proofEngineTypes.cmi 
+proofEngineTypes.cmo: proofEngineTypes.cmi 
+proofEngineTypes.cmx: proofEngineTypes.cmi 
+proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
+proofEngineHelpers.cmx: proofEngineTypes.cmx proofEngineHelpers.cmi 
+proofEngineReduction.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \
+    proofEngineReduction.cmi 
+proofEngineReduction.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \
+    proofEngineReduction.cmi 
+continuationals.cmo: proofEngineTypes.cmi continuationals.cmi 
+continuationals.cmx: proofEngineTypes.cmx continuationals.cmi 
+tacticals.cmo: proofEngineTypes.cmi continuationals.cmi tacticals.cmi 
+tacticals.cmx: proofEngineTypes.cmx continuationals.cmx tacticals.cmi 
+reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \
+    proofEngineHelpers.cmi reductionTactics.cmi 
+reductionTactics.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \
+    proofEngineHelpers.cmx reductionTactics.cmi 
+proofEngineStructuralRules.cmo: proofEngineTypes.cmi \
+    proofEngineStructuralRules.cmi 
+proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
+    proofEngineStructuralRules.cmi 
+primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi 
+primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi 
+hashtbl_equiv.cmo: hashtbl_equiv.cmi 
+hashtbl_equiv.cmx: hashtbl_equiv.cmi 
+metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
+    hashtbl_equiv.cmi metadataQuery.cmi 
+metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
+    hashtbl_equiv.cmx metadataQuery.cmi 
+universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi 
+universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi 
+autoTypes.cmo: autoTypes.cmi 
+autoTypes.cmx: autoTypes.cmi 
+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 
+paramodulation/subst.cmo: paramodulation/subst.cmi 
+paramodulation/subst.cmx: paramodulation/subst.cmi 
+paramodulation/equality.cmo: paramodulation/utils.cmi \
+    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
+    paramodulation/equality.cmi 
+paramodulation/equality.cmx: paramodulation/utils.cmx \
+    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
+    paramodulation/equality.cmi 
+paramodulation/founif.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \
+    paramodulation/founif.cmi 
+paramodulation/founif.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \
+    paramodulation/founif.cmi 
+paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
+    paramodulation/equality.cmi paramodulation/equality_indexing.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/equality_indexing.cmi paramodulation/equality.cmi \
+    paramodulation/indexing.cmi 
+paramodulation/indexing.cmx: paramodulation/utils.cmx \
+    paramodulation/subst.cmx paramodulation/founif.cmx \
+    paramodulation/equality_indexing.cmx paramodulation/equality.cmx \
+    paramodulation/indexing.cmi 
+paramodulation/saturation.cmo: paramodulation/utils.cmi \
+    paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
+    paramodulation/indexing.cmi paramodulation/founif.cmi \
+    paramodulation/equality.cmi paramodulation/saturation.cmi 
+paramodulation/saturation.cmx: paramodulation/utils.cmx \
+    paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
+    paramodulation/indexing.cmx paramodulation/founif.cmx \
+    paramodulation/equality.cmx paramodulation/saturation.cmi 
+variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
+    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+    variousTactics.cmi 
+variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
+    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+    variousTactics.cmi 
+introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
+    introductionTactics.cmi 
+introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
+    introductionTactics.cmi 
+eliminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
+    proofEngineTypes.cmi proofEngineStructuralRules.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi eliminationTactics.cmi 
+eliminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
+    proofEngineTypes.cmx proofEngineStructuralRules.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmx eliminationTactics.cmi 
+negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \
+    primitiveTactics.cmi eliminationTactics.cmi negationTactics.cmi 
+negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \
+    primitiveTactics.cmx eliminationTactics.cmx negationTactics.cmi 
+equalityTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+    proofEngineStructuralRules.cmi proofEngineReduction.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \
+    equalityTactics.cmi 
+equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+    proofEngineStructuralRules.cmx proofEngineReduction.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
+    equalityTactics.cmi 
+auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/subst.cmi \
+    paramodulation/saturation.cmi proofEngineTypes.cmi \
+    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+    metadataQuery.cmi paramodulation/indexing.cmi equalityTactics.cmi \
+    paramodulation/equality.cmi autoTypes.cmi autoCache.cmi auto.cmi 
+auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
+    paramodulation/saturation.cmx proofEngineTypes.cmx \
+    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+    metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
+    paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi 
+autoTactic.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \
+    primitiveTactics.cmi metadataQuery.cmi paramodulation/equality.cmi \
+    autoTypes.cmi auto.cmi autoTactic.cmi 
+autoTactic.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \
+    primitiveTactics.cmx metadataQuery.cmx paramodulation/equality.cmx \
+    autoTypes.cmx auto.cmx autoTactic.cmi 
+discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
+    proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
+    introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \
+    discriminationTactics.cmi 
+discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
+    proofEngineTypes.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
+    introductionTactics.cmx equalityTactics.cmx eliminationTactics.cmx \
+    discriminationTactics.cmi 
+inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+    equalityTactics.cmi inversion.cmi 
+inversion.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+    equalityTactics.cmx inversion.cmi 
+inversion_principle.cmo: tacticals.cmi proofEngineTypes.cmi \
+    primitiveTactics.cmi inversion.cmi inversion_principle.cmi 
+inversion_principle.cmx: tacticals.cmx proofEngineTypes.cmx \
+    primitiveTactics.cmx inversion.cmx inversion_principle.cmi 
+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 
+fourier.cmo: fourier.cmi 
+fourier.cmx: fourier.cmi 
+fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \
+    proofEngineTypes.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+    fourier.cmi equalityTactics.cmi fourierR.cmi 
+fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \
+    proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+    fourier.cmx equalityTactics.cmx fourierR.cmi 
+fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi \
+    proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
+    primitiveTactics.cmi fwdSimplTactic.cmi 
+fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx \
+    proofEngineStructuralRules.cmx proofEngineHelpers.cmx \
+    primitiveTactics.cmx fwdSimplTactic.cmi 
+history.cmo: history.cmi 
+history.cmx: history.cmi 
+statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \
+    statefulProofEngine.cmi 
+statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \
+    statefulProofEngine.cmi 
+tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi ring.cmi \
+    reductionTactics.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
+    negationTactics.cmi inversion.cmi introductionTactics.cmi \
+    fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \
+    eliminationTactics.cmi discriminationTactics.cmi autoTactic.cmi auto.cmi \
+    tactics.cmi 
+tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
+    reductionTactics.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
+    negationTactics.cmx inversion.cmx introductionTactics.cmx \
+    fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
+    eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \
+    tactics.cmi 
+declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+    declarative.cmi 
+declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+    declarative.cmi 

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 6d842a79717f4d74ac8f1313e6d1f14b3914f572..71265bc7a026959a28b3c761cb8dbedd91ae16db 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Dec 29 00:00:27 CET 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Dec 29 14:56:56 CET 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :

diff --git a/helm/software/components/thread/.depend.opt b/helm/software/components/thread/.depend.opt
new file mode 100644 (file)
index 0000000..7759190
--- /dev/null
+++ b/helm/software/components/thread/.depend.opt
@@ -0,0 +1,4 @@
+threadSafe.cmo: threadSafe.cmi 
+threadSafe.cmx: threadSafe.cmi 
+extThread.cmo: extThread.cmi 
+extThread.cmx: extThread.cmi 

diff --git a/helm/software/components/tptp_grafite/.depend.opt b/helm/software/components/tptp_grafite/.depend.opt
new file mode 100644 (file)
index 0000000..c743002
--- /dev/null
+++ b/helm/software/components/tptp_grafite/.depend.opt
@@ -0,0 +1,7 @@
+parser.cmi: ast.cmx 
+lexer.cmo: parser.cmi 
+lexer.cmx: parser.cmx 
+parser.cmo: ast.cmx parser.cmi 
+parser.cmx: ast.cmx parser.cmi 
+tptp2grafite.cmo: parser.cmi lexer.cmx ast.cmx tptp2grafite.cmi 
+tptp2grafite.cmx: parser.cmx lexer.cmx ast.cmx tptp2grafite.cmi 

diff --git a/helm/software/components/urimanager/.depend.opt b/helm/software/components/urimanager/.depend.opt
new file mode 100644 (file)
index 0000000..4821484
--- /dev/null
+++ b/helm/software/components/urimanager/.depend.opt
@@ -0,0 +1,2 @@
+uriManager.cmo: uriManager.cmi 
+uriManager.cmx: uriManager.cmi 

diff --git a/helm/software/components/whelp/.depend.opt b/helm/software/components/whelp/.depend.opt
new file mode 100644 (file)
index 0000000..39f37df
--- /dev/null
+++ b/helm/software/components/whelp/.depend.opt
@@ -0,0 +1,4 @@
+whelp.cmo: whelp.cmi 
+whelp.cmx: whelp.cmi 
+fwdQueries.cmo: fwdQueries.cmi 
+fwdQueries.cmx: fwdQueries.cmi 

diff --git a/helm/software/components/xml/.depend.opt b/helm/software/components/xml/.depend.opt
new file mode 100644 (file)
index 0000000..5ef59bd
--- /dev/null
+++ b/helm/software/components/xml/.depend.opt
@@ -0,0 +1,4 @@
+xml.cmo: xml.cmi 
+xml.cmx: xml.cmi 
+xmlPushParser.cmo: xmlPushParser.cmi 
+xmlPushParser.cmx: xmlPushParser.cmi 

diff --git a/helm/software/components/xmldiff/.depend.opt b/helm/software/components/xmldiff/.depend.opt
new file mode 100644 (file)
index 0000000..e2832de
--- /dev/null
+++ b/helm/software/components/xmldiff/.depend.opt
@@ -0,0 +1,2 @@
+xmlDiff.cmo: xmlDiff.cmi 
+xmlDiff.cmx: xmlDiff.cmi 

diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt
new file mode 100644 (file)
index 0000000..7860c2d
--- /dev/null
+++ b/helm/software/matita/.depend.opt
@@ -0,0 +1,73 @@
+applyTransformation.cmo: applyTransformation.cmi 
+applyTransformation.cmx: applyTransformation.cmi 
+buildTimeConf.cmo: buildTimeConf.cmi 
+buildTimeConf.cmx: buildTimeConf.cmi 
+dump_moo.cmo: buildTimeConf.cmi 
+dump_moo.cmx: buildTimeConf.cmx 
+gragrep.cmo: matitaInit.cmi buildTimeConf.cmi gragrep.cmi 
+gragrep.cmx: matitaInit.cmx buildTimeConf.cmx gragrep.cmi 
+lablGraphviz.cmo: lablGraphviz.cmi 
+lablGraphviz.cmx: lablGraphviz.cmi 
+matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi 
+matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi 
+matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \
+    matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi 
+matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \
+    matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi 
+matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \
+    matitacLib.cmi gragrep.cmi 
+matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \
+    matitacLib.cmx gragrep.cmx 
+matitadep.cmo: matitaInit.cmi matitadep.cmi 
+matitadep.cmx: matitaInit.cmx matitadep.cmi 
+matitaEngine.cmo: matitaEngine.cmi 
+matitaEngine.cmx: matitaEngine.cmi 
+matitaExcPp.cmo: matitaExcPp.cmi 
+matitaExcPp.cmx: matitaExcPp.cmi 
+matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmi \
+    matitaGtkMisc.cmi 
+matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
+    matitaGtkMisc.cmi 
+matitaGui.cmo: matitaprover.cmi matitamakeLib.cmi matitaTypes.cmi \
+    matitaScript.cmi matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \
+    matitaGeneratedGui.cmx matitaExcPp.cmi buildTimeConf.cmi matitaGui.cmi 
+matitaGui.cmx: matitaprover.cmx matitamakeLib.cmx matitaTypes.cmx \
+    matitaScript.cmx matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \
+    matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi 
+matitaInit.cmo: matitamakeLib.cmi buildTimeConf.cmi matitaInit.cmi 
+matitaInit.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaInit.cmi 
+matitamakeLib.cmo: buildTimeConf.cmi matitamakeLib.cmi 
+matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi 
+matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmi 
+matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitamake.cmi 
+matitaMathView.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \
+    matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \
+    lablGraphviz.cmi buildTimeConf.cmi applyTransformation.cmi \
+    matitaMathView.cmi 
+matitaMathView.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \
+    matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \
+    lablGraphviz.cmx buildTimeConf.cmx applyTransformation.cmx \
+    matitaMathView.cmi 
+matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi 
+matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi 
+matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \
+    matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi 
+matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \
+    matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx 
+matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
+    buildTimeConf.cmi matitaprover.cmi 
+matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
+    buildTimeConf.cmx matitaprover.cmi 
+matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \
+    matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmi \
+    applyTransformation.cmi matitaScript.cmi 
+matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \
+    matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \
+    applyTransformation.cmx matitaScript.cmi 
+matitaTypes.cmo: matitaTypes.cmi 
+matitaTypes.cmx: matitaTypes.cmi 
+matitaGtkMisc.cmi: matitaGeneratedGui.cmx 
+matitaGui.cmi: matitaGuiTypes.cmi 
+matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx 
+matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi 
+matitaScript.cmi: matitaTypes.cmi 

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index fd96cc5f99d7ebd4cf2ba79d9c411731ae073f77..c0e31d64315558d6709e900a60e58f7429f9aed7 100644 (file)
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -385,12 +385,18 @@ depend:
        $(H)$(OCAMLDEP) *.ml *.mli > .depend
 depend.opt:
        $(H)echo "  OCAMLDEP -native"
-       $(H)$(OCAMLDEP) -native *.ml *.mli > .depend
+       $(H)$(OCAMLDEP) -native *.ml *.mli > .depend.opt
 
-ifneq ($(MAKECMDGOALS), depend)
- ifneq ($(MAKECMDGOALS), depend.opt)
-   include .depend   
- endif
+ifeq ($(MAKECMDGOALS),)
+  include .depend   
+endif
+
+ifeq ($(MAKECMDGOALS), all)
+  include .depend   
+endif
+
+ifeq ($(MAKECMDGOALS), opt)
+  include .depend.opt   
 endif
 
 %.cmi: %.mli