From: Ferruccio Guidi Date: Fri, 29 Dec 2006 14:35:31 +0000 (+0000) Subject: now we try two distinct depend files for compilation in byte and native code X-Git-Tag: 0.4.95@7852~698 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e32fcdcb9ba66f4b3a31f283dc24fbe5dccb398;p=helm.git now we try two distinct depend files for compilation in byte and native code --- diff --git a/components/Makefile.common b/components/Makefile.common index b6ad6eb96..30bd4c889 100644 --- a/components/Makefile.common +++ b/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/components/acic_content/.depend.opt b/components/acic_content/.depend.opt new file mode 100644 index 000000000..fef879256 --- /dev/null +++ b/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/components/binaries/extractor/.depend.opt b/components/binaries/extractor/.depend.opt new file mode 100644 index 000000000..e69de29bb diff --git a/components/binaries/extractor/Makefile b/components/binaries/extractor/Makefile index f7151e3cb..eae5c635d 100644 --- a/components/binaries/extractor/Makefile +++ b/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/components/binaries/saturate/Makefile b/components/binaries/saturate/Makefile index 567e3b0d3..ecd8d9111 100644 --- a/components/binaries/saturate/Makefile +++ b/components/binaries/saturate/Makefile @@ -28,5 +28,6 @@ clean: $(H)rm -f saturate saturate.opt depend: +depend.opt: include ../../../Makefile.defs diff --git a/components/binaries/table_creator/.depend.opt b/components/binaries/table_creator/.depend.opt new file mode 100644 index 000000000..e69de29bb diff --git a/components/binaries/table_creator/Makefile b/components/binaries/table_creator/Makefile index 15cf1863a..23e732629 100644 --- a/components/binaries/table_creator/Makefile +++ b/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/components/binaries/utilities/.depend.opt b/components/binaries/utilities/.depend.opt new file mode 100644 index 000000000..e69de29bb diff --git a/components/binaries/utilities/Makefile b/components/binaries/utilities/Makefile index 314136db5..1874a2385 100644 --- a/components/binaries/utilities/Makefile +++ b/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/components/cic/.depend.opt b/components/cic/.depend.opt new file mode 100644 index 000000000..44b016d1c --- /dev/null +++ b/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/components/cic_acic/.depend.opt b/components/cic_acic/.depend.opt new file mode 100644 index 000000000..3fc1e0dce --- /dev/null +++ b/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/components/cic_disambiguation/.depend.opt b/components/cic_disambiguation/.depend.opt new file mode 100644 index 000000000..ca4124461 --- /dev/null +++ b/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/components/cic_proof_checking/.depend.opt b/components/cic_proof_checking/.depend.opt new file mode 100644 index 000000000..06b9188a0 --- /dev/null +++ b/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/components/cic_unification/.depend.opt b/components/cic_unification/.depend.opt new file mode 100644 index 000000000..9fa71a619 --- /dev/null +++ b/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/components/content_pres/.depend b/components/content_pres/.depend index d2bd17f19..759898ac6 100644 --- a/components/content_pres/.depend +++ b/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/components/content_pres/.depend.opt b/components/content_pres/.depend.opt new file mode 100644 index 000000000..759898ac6 --- /dev/null +++ b/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/components/extlib/.depend.opt b/components/extlib/.depend.opt new file mode 100644 index 000000000..6d96e61e2 --- /dev/null +++ b/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/components/getter/.depend.opt b/components/getter/.depend.opt new file mode 100644 index 000000000..554fb1ec7 --- /dev/null +++ b/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/components/grafite/.depend.opt b/components/grafite/.depend.opt new file mode 100644 index 000000000..0f64ba789 --- /dev/null +++ b/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/components/grafite_engine/.depend.opt b/components/grafite_engine/.depend.opt new file mode 100644 index 000000000..b0d4b7048 --- /dev/null +++ b/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/components/grafite_parser/.depend.opt b/components/grafite_parser/.depend.opt new file mode 100644 index 000000000..2dc8a7cab --- /dev/null +++ b/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/components/hgdome/.depend.opt b/components/hgdome/.depend.opt new file mode 100644 index 000000000..bf9c09af7 --- /dev/null +++ b/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/components/hmysql/.depend.opt b/components/hmysql/.depend.opt new file mode 100644 index 000000000..e67a0660c --- /dev/null +++ b/components/hmysql/.depend.opt @@ -0,0 +1,2 @@ +hMysql.cmo: hMysql.cmi +hMysql.cmx: hMysql.cmi diff --git a/components/lexicon/.depend.opt b/components/lexicon/.depend.opt new file mode 100644 index 000000000..7fec1d3b5 --- /dev/null +++ b/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/components/library/.depend.opt b/components/library/.depend.opt new file mode 100644 index 000000000..eacb26990 --- /dev/null +++ b/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/components/logger/.depend.opt b/components/logger/.depend.opt new file mode 100644 index 000000000..28268d29e --- /dev/null +++ b/components/logger/.depend.opt @@ -0,0 +1,2 @@ +helmLogger.cmo: helmLogger.cmi +helmLogger.cmx: helmLogger.cmi diff --git a/components/metadata/.depend.opt b/components/metadata/.depend.opt new file mode 100644 index 000000000..492a34e3a --- /dev/null +++ b/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/components/registry/.depend.opt b/components/registry/.depend.opt new file mode 100644 index 000000000..cf4f36b68 --- /dev/null +++ b/components/registry/.depend.opt @@ -0,0 +1,2 @@ +helm_registry.cmo: helm_registry.cmi +helm_registry.cmx: helm_registry.cmi diff --git a/components/syntax_extensions/.depend.opt b/components/syntax_extensions/.depend.opt new file mode 100644 index 000000000..c0cd9c906 --- /dev/null +++ b/components/syntax_extensions/.depend.opt @@ -0,0 +1,2 @@ +utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/components/tactics/.depend.opt b/components/tactics/.depend.opt new file mode 100644 index 000000000..6c23fc909 --- /dev/null +++ b/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/components/tactics/tactics.mli b/components/tactics/tactics.mli index 6d842a797..71265bc7a 100644 --- a/components/tactics/tactics.mli +++ b/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/components/thread/.depend.opt b/components/thread/.depend.opt new file mode 100644 index 000000000..7759190c6 --- /dev/null +++ b/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/components/tptp_grafite/.depend.opt b/components/tptp_grafite/.depend.opt new file mode 100644 index 000000000..c74300207 --- /dev/null +++ b/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/components/urimanager/.depend.opt b/components/urimanager/.depend.opt new file mode 100644 index 000000000..482148423 --- /dev/null +++ b/components/urimanager/.depend.opt @@ -0,0 +1,2 @@ +uriManager.cmo: uriManager.cmi +uriManager.cmx: uriManager.cmi diff --git a/components/whelp/.depend.opt b/components/whelp/.depend.opt new file mode 100644 index 000000000..39f37dfa9 --- /dev/null +++ b/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/components/xml/.depend.opt b/components/xml/.depend.opt new file mode 100644 index 000000000..5ef59bdc9 --- /dev/null +++ b/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/components/xmldiff/.depend.opt b/components/xmldiff/.depend.opt new file mode 100644 index 000000000..e2832de33 --- /dev/null +++ b/components/xmldiff/.depend.opt @@ -0,0 +1,2 @@ +xmlDiff.cmo: xmlDiff.cmi +xmlDiff.cmx: xmlDiff.cmi diff --git a/matita/.depend.opt b/matita/.depend.opt new file mode 100644 index 000000000..7860c2d16 --- /dev/null +++ b/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/matita/Makefile b/matita/Makefile index fd96cc5f9..c0e31d643 100644 --- a/matita/Makefile +++ b/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