added auto_cache in the dupable status after an

re-factoring and re-typing of the whole serialization
code.

diff --git a/helm/software/components/METAS/meta.helm-grafite_parser.src b/helm/software/components/METAS/meta.helm-grafite_parser.src
index a214a83dcd4df02683e835bfb847b0343d08243c..bcde338d3114a1f887daa1e4045b226336243c0e 100644 (file)
--- a/helm/software/components/METAS/meta.helm-grafite_parser.src
+++ b/helm/software/components/METAS/meta.helm-grafite_parser.src
@@ -1,4 +1,4 @@
-requires="helm-lexicon helm-grafite ulex08 helm-ng_disambiguation"
+requires="helm-lexicon helm-grafite ulex08 helm-ng_disambiguation helm-ng_library"
 version="0.0.1"
 archive(byte)="grafite_parser.cma"
 archive(native)="grafite_parser.cmxa"

diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile
index 25169744f5a39ab09c3da94a4b92b7649bb4eb48..e12688b64eb591ab94517691b1e76300297d9864 100644 (file)
--- a/helm/software/components/Makefile
+++ b/helm/software/components/Makefile
@@ -38,14 +38,14 @@ MODULES =                   \
        cic_disambiguation      \
        lexicon                 \
        ng_disambiguation       \
-       grafite_parser          \
        ng_paramodulation       \
-       ng_tactics              \
-       grafite_engine          \
        tptp_grafite            \
        ng_kernel               \
        ng_refiner              \
-       ng_library                                                      \
+       ng_library              \
+       grafite_parser          \
+       ng_tactics              \
+       grafite_engine          \
        $(NULL)
 
 METAS = $(MODULES:%=METAS/META.helm-%)

diff --git a/helm/software/components/acic_content/.depend b/helm/software/components/acic_content/.depend
index 8ade458af771b340426f4e4606d92e511c459a56..89dca0e446d48d1f05a1cda5fc3c39f1095257e3 100644 (file)
--- a/helm/software/components/acic_content/.depend
+++ b/helm/software/components/acic_content/.depend
@@ -1,3 +1,4 @@
+content.cmi: 
 acic2content.cmi: content.cmi 
 content2cic.cmi: content.cmi 
 cicNotationUtil.cmi: cicNotationPt.cmo 
@@ -5,6 +6,8 @@ cicNotationEnv.cmi: cicNotationPt.cmo
 cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi 
 acic2astMatcher.cmi: cicNotationPt.cmo 
 termAcicContent.cmi: cicNotationPt.cmo 
+cicNotationPt.cmo: 
+cicNotationPt.cmx: 
 content.cmo: content.cmi 
 content.cmx: content.cmi 
 acic2content.cmo: content.cmi acic2content.cmi 

diff --git a/helm/software/components/acic_content/.depend.opt b/helm/software/components/acic_content/.depend.opt
index fef8792567075850eb766452dd005034b8a354f9..307fceaa0288ab3dec50b1407588d9cb67d84bb5 100644 (file)
--- a/helm/software/components/acic_content/.depend.opt
+++ b/helm/software/components/acic_content/.depend.opt
@@ -1,3 +1,4 @@
+content.cmi: 
 acic2content.cmi: content.cmi 
 content2cic.cmi: content.cmi 
 cicNotationUtil.cmi: cicNotationPt.cmx 
@@ -5,6 +6,8 @@ cicNotationEnv.cmi: cicNotationPt.cmx
 cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi 
 acic2astMatcher.cmi: cicNotationPt.cmx 
 termAcicContent.cmi: cicNotationPt.cmx 
+cicNotationPt.cmo: 
+cicNotationPt.cmx: 
 content.cmo: content.cmi 
 content.cmx: content.cmi 
 acic2content.cmo: content.cmi acic2content.cmi 

diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend
index 8d0128744c8b9e740462a1a8001764036199a67e..97238c4d861fc8ee80cbafc6c9c6337d3e3babf2 100644 (file)
--- a/helm/software/components/acic_procedural/.depend
+++ b/helm/software/components/acic_procedural/.depend
@@ -1,6 +1,13 @@
+proceduralHelpers.cmi: 
+proceduralClassify.cmi: 
+proceduralOptimizer.cmi: 
+proceduralTypes.cmi: 
+proceduralMode.cmi: 
+proceduralConversion.cmi: 
 procedural1.cmi: proceduralTypes.cmi 
 procedural2.cmi: proceduralTypes.cmi 
 proceduralTeX.cmi: proceduralTypes.cmi 
+acic2Procedural.cmi: 
 proceduralHelpers.cmo: proceduralHelpers.cmi 
 proceduralHelpers.cmx: proceduralHelpers.cmi 
 proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi 

diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt
index 8d0128744c8b9e740462a1a8001764036199a67e..97238c4d861fc8ee80cbafc6c9c6337d3e3babf2 100644 (file)
--- a/helm/software/components/acic_procedural/.depend.opt
+++ b/helm/software/components/acic_procedural/.depend.opt
@@ -1,6 +1,13 @@
+proceduralHelpers.cmi: 
+proceduralClassify.cmi: 
+proceduralOptimizer.cmi: 
+proceduralTypes.cmi: 
+proceduralMode.cmi: 
+proceduralConversion.cmi: 
 procedural1.cmi: proceduralTypes.cmi 
 procedural2.cmi: proceduralTypes.cmi 
 proceduralTeX.cmi: proceduralTypes.cmi 
+acic2Procedural.cmi: 
 proceduralHelpers.cmo: proceduralHelpers.cmi 
 proceduralHelpers.cmx: proceduralHelpers.cmi 
 proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi 

diff --git a/helm/software/components/binaries/extractor/.depend b/helm/software/components/binaries/extractor/.depend
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0c39328ae147e8ab714b2d3a7b1582a011b2b1d6 100644 (file)
--- a/helm/software/components/binaries/extractor/.depend
+++ b/helm/software/components/binaries/extractor/.depend
@@ -0,0 +1,4 @@
+extractor.cmo: 
+extractor.cmx: 
+extractor_manager.cmo: 
+extractor_manager.cmx: 

diff --git a/helm/software/components/binaries/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0c39328ae147e8ab714b2d3a7b1582a011b2b1d6 100644 (file)
--- a/helm/software/components/binaries/extractor/.depend.opt
+++ b/helm/software/components/binaries/extractor/.depend.opt
@@ -0,0 +1,4 @@
+extractor.cmo: 
+extractor.cmx: 
+extractor_manager.cmo: 
+extractor_manager.cmx: 

diff --git a/helm/software/components/binaries/table_creator/.depend b/helm/software/components/binaries/table_creator/.depend
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..33147b94948d28fc9c7132773964d2547472c2ba 100644 (file)
--- a/helm/software/components/binaries/table_creator/.depend
+++ b/helm/software/components/binaries/table_creator/.depend
@@ -0,0 +1,2 @@
+table_creator.cmo: 
+table_creator.cmx: 

diff --git a/helm/software/components/binaries/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..33147b94948d28fc9c7132773964d2547472c2ba 100644 (file)
--- a/helm/software/components/binaries/table_creator/.depend.opt
+++ b/helm/software/components/binaries/table_creator/.depend.opt
@@ -0,0 +1,2 @@
+table_creator.cmo: 
+table_creator.cmx: 

diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend
index bb6f22a64b02f88c3881f2c3f490d7f81b186897..87d1ed25c2745435771cee189c10da4a99854448 100644 (file)
--- a/helm/software/components/binaries/transcript/.depend
+++ b/helm/software/components/binaries/transcript/.depend
@@ -1,6 +1,11 @@
 gallina8Parser.cmi: types.cmo 
 grafiteParser.cmi: types.cmo 
 grafite.cmi: types.cmo 
+engine.cmi: 
+types.cmo: 
+types.cmx: 
+options.cmo: 
+options.cmx: 
 gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi 
 gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Lexer.cmo: options.cmo gallina8Parser.cmi 

diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt
index efadc681eee16cb3cd170845fdd1c7549fbb89b0..f17459162ce81c0ad9c5352cca5e9d99f43cb81c 100644 (file)
--- a/helm/software/components/binaries/transcript/.depend.opt
+++ b/helm/software/components/binaries/transcript/.depend.opt
@@ -1,6 +1,11 @@
 gallina8Parser.cmi: types.cmx 
 grafiteParser.cmi: types.cmx 
 grafite.cmi: types.cmx 
+engine.cmi: 
+types.cmo: 
+types.cmx: 
+options.cmo: 
+options.cmx: 
 gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Lexer.cmo: options.cmx gallina8Parser.cmi 

diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend
index c2c7105c727f1c8101a1a119d3521629984d3dcf..a835b247f3b3006e53a73a62b9ff56d394eca590 100644 (file)
--- a/helm/software/components/cic/.depend
+++ b/helm/software/components/cic/.depend
@@ -1,8 +1,10 @@
+cicUniv.cmi: 
 unshare.cmi: cic.cmo 
 deannotate.cmi: cic.cmo 
 cicParser.cmi: cic.cmo 
 cicUtil.cmi: cic.cmo 
 helmLibraryObjects.cmi: cic.cmo 
+libraryObjects.cmi: 
 cic_indexable.cmi: cic.cmo 
 path_indexing.cmi: cic.cmo 
 cicInspect.cmi: cic.cmo 

diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt
index 76d19c1ff002243a04033cccc16ff71f291e5167..8cdd2a86aa5532872a81f4bf977cb65500389620 100644 (file)
--- a/helm/software/components/cic/.depend.opt
+++ b/helm/software/components/cic/.depend.opt
@@ -1,8 +1,10 @@
+cicUniv.cmi: 
 unshare.cmi: cic.cmx 
 deannotate.cmi: cic.cmx 
 cicParser.cmi: cic.cmx 
 cicUtil.cmi: cic.cmx 
 helmLibraryObjects.cmi: cic.cmx 
+libraryObjects.cmi: 
 cic_indexable.cmi: cic.cmx 
 path_indexing.cmi: cic.cmx 
 cicInspect.cmi: cic.cmx 

diff --git a/helm/software/components/cic_acic/.depend b/helm/software/components/cic_acic/.depend
index 3fc1e0dce9eedda1f0bb74a669ad175582f03e06..5449d50aaa2d43c1a8126f0561177e904f0975da 100644 (file)
--- a/helm/software/components/cic_acic/.depend
+++ b/helm/software/components/cic_acic/.depend
@@ -1,3 +1,6 @@
+eta_fixing.cmi: 
+doubleTypeInference.cmi: 
+cic2acic.cmi: 
 cic2Xml.cmi: cic2acic.cmi 
 eta_fixing.cmo: eta_fixing.cmi 
 eta_fixing.cmx: eta_fixing.cmi 

diff --git a/helm/software/components/cic_acic/.depend.opt b/helm/software/components/cic_acic/.depend.opt
index 3fc1e0dce9eedda1f0bb74a669ad175582f03e06..5449d50aaa2d43c1a8126f0561177e904f0975da 100644 (file)
--- a/helm/software/components/cic_acic/.depend.opt
+++ b/helm/software/components/cic_acic/.depend.opt
@@ -1,3 +1,6 @@
+eta_fixing.cmi: 
+doubleTypeInference.cmi: 
+cic2acic.cmi: 
 cic2Xml.cmi: cic2acic.cmi 
 eta_fixing.cmo: eta_fixing.cmi 
 eta_fixing.cmx: eta_fixing.cmi 

diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend
index e9bd1168f73e4e834b02480bca0e67e381fc4997..a9ae65a5e3c4c3df2f8aaca3b2762c794bee6bd5 100644 (file)
--- a/helm/software/components/cic_disambiguation/.depend
+++ b/helm/software/components/cic_disambiguation/.depend
@@ -1,3 +1,5 @@
+cicDisambiguate.cmi: 
+disambiguateChoices.cmi: 
 cicDisambiguate.cmo: cicDisambiguate.cmi 
 cicDisambiguate.cmx: cicDisambiguate.cmi 
 disambiguateChoices.cmo: disambiguateChoices.cmi 

diff --git a/helm/software/components/cic_disambiguation/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt
index e9bd1168f73e4e834b02480bca0e67e381fc4997..a9ae65a5e3c4c3df2f8aaca3b2762c794bee6bd5 100644 (file)
--- a/helm/software/components/cic_disambiguation/.depend.opt
+++ b/helm/software/components/cic_disambiguation/.depend.opt
@@ -1,3 +1,5 @@
+cicDisambiguate.cmi: 
+disambiguateChoices.cmi: 
 cicDisambiguate.cmo: cicDisambiguate.cmi 
 cicDisambiguate.cmx: cicDisambiguate.cmi 
 disambiguateChoices.cmo: disambiguateChoices.cmi 

diff --git a/helm/software/components/cic_exportation/.depend b/helm/software/components/cic_exportation/.depend
index 288ea5f6cf50f1cb6bb8ff00d53a0262825c3459..91be8d88d36bf6f3df5cd920db6a75f80a5ff64d 100644 (file)
--- a/helm/software/components/cic_exportation/.depend
+++ b/helm/software/components/cic_exportation/.depend
@@ -1,2 +1,3 @@
+cicExportation.cmi: 
 cicExportation.cmo: cicExportation.cmi 
 cicExportation.cmx: cicExportation.cmi 

diff --git a/helm/software/components/cic_exportation/.depend.opt b/helm/software/components/cic_exportation/.depend.opt
index 288ea5f6cf50f1cb6bb8ff00d53a0262825c3459..91be8d88d36bf6f3df5cd920db6a75f80a5ff64d 100644 (file)
--- a/helm/software/components/cic_exportation/.depend.opt
+++ b/helm/software/components/cic_exportation/.depend.opt
@@ -1,2 +1,3 @@
+cicExportation.cmi: 
 cicExportation.cmo: cicExportation.cmi 
 cicExportation.cmx: cicExportation.cmi 

diff --git a/helm/software/components/cic_proof_checking/.depend b/helm/software/components/cic_proof_checking/.depend
index 5d83fd0f3d146e2d80ead2d8eb5c34b162a5835f..f8a16629ebd091a0c9e60b948c7e2eedb8908a16 100644 (file)
--- a/helm/software/components/cic_proof_checking/.depend
+++ b/helm/software/components/cic_proof_checking/.depend
@@ -1,3 +1,13 @@
+cicLogger.cmi: 
+cicEnvironment.cmi: 
+cicPp.cmi: 
+cicUnivUtils.cmi: 
+cicSubstitution.cmi: 
+cicMiniReduction.cmi: 
+cicReduction.cmi: 
+cicTypeChecker.cmi: 
+freshNamesGenerator.cmi: 
+cicDischarge.cmi: 
 cicLogger.cmo: cicLogger.cmi 
 cicLogger.cmx: cicLogger.cmi 
 cicEnvironment.cmo: cicEnvironment.cmi 

diff --git a/helm/software/components/cic_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt
index 5d83fd0f3d146e2d80ead2d8eb5c34b162a5835f..f8a16629ebd091a0c9e60b948c7e2eedb8908a16 100644 (file)
--- a/helm/software/components/cic_proof_checking/.depend.opt
+++ b/helm/software/components/cic_proof_checking/.depend.opt
@@ -1,3 +1,13 @@
+cicLogger.cmi: 
+cicEnvironment.cmi: 
+cicPp.cmi: 
+cicUnivUtils.cmi: 
+cicSubstitution.cmi: 
+cicMiniReduction.cmi: 
+cicReduction.cmi: 
+cicTypeChecker.cmi: 
+freshNamesGenerator.cmi: 
+cicDischarge.cmi: 
 cicLogger.cmo: cicLogger.cmi 
 cicLogger.cmx: cicLogger.cmi 
 cicEnvironment.cmo: cicEnvironment.cmi 

diff --git a/helm/software/components/cic_unification/.depend b/helm/software/components/cic_unification/.depend
index a7b23ceb4e8ba6ae3fdc2fa8352ce69acbde78b0..2e054f73d4e69376cc89138609538274bd8fe6d8 100644 (file)
--- a/helm/software/components/cic_unification/.depend
+++ b/helm/software/components/cic_unification/.depend
@@ -1,3 +1,10 @@
+cicMetaSubst.cmi: 
+cicMkImplicit.cmi: 
+termUtil.cmi: 
+coercGraph.cmi: 
+cicUnification.cmi: 
+cicReplace.cmi: 
+cicRefine.cmi: 
 cicMetaSubst.cmo: cicMetaSubst.cmi 
 cicMetaSubst.cmx: cicMetaSubst.cmi 
 cicMkImplicit.cmo: cicMkImplicit.cmi 

diff --git a/helm/software/components/cic_unification/.depend.opt b/helm/software/components/cic_unification/.depend.opt
index a7b23ceb4e8ba6ae3fdc2fa8352ce69acbde78b0..2e054f73d4e69376cc89138609538274bd8fe6d8 100644 (file)
--- a/helm/software/components/cic_unification/.depend.opt
+++ b/helm/software/components/cic_unification/.depend.opt
@@ -1,3 +1,10 @@
+cicMetaSubst.cmi: 
+cicMkImplicit.cmi: 
+termUtil.cmi: 
+coercGraph.cmi: 
+cicUnification.cmi: 
+cicReplace.cmi: 
+cicRefine.cmi: 
 cicMetaSubst.cmo: cicMetaSubst.cmi 
 cicMetaSubst.cmx: cicMetaSubst.cmi 
 cicMkImplicit.cmo: cicMkImplicit.cmi 

diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend
index 6dd0e78a19212937b664b03fb796d8aaf496dbbb..8d74439eb72834455b6f06006f1f5534312a3a51 100644 (file)
--- a/helm/software/components/content_pres/.depend
+++ b/helm/software/components/content_pres/.depend
@@ -1,3 +1,9 @@
+renderingAttrs.cmi: 
+cicNotationLexer.cmi: 
+cicNotationParser.cmi: 
+mpresentation.cmi: 
+box.cmi: 
+content2presMatcher.cmi: 
 termContentPres.cmi: cicNotationParser.cmi 
 boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi 
 cicNotationPres.cmi: mpresentation.cmi box.cmi 

diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt
index 6dd0e78a19212937b664b03fb796d8aaf496dbbb..8d74439eb72834455b6f06006f1f5534312a3a51 100644 (file)
--- a/helm/software/components/content_pres/.depend.opt
+++ b/helm/software/components/content_pres/.depend.opt
@@ -1,3 +1,9 @@
+renderingAttrs.cmi: 
+cicNotationLexer.cmi: 
+cicNotationParser.cmi: 
+mpresentation.cmi: 
+box.cmi: 
+content2presMatcher.cmi: 
 termContentPres.cmi: cicNotationParser.cmi 
 boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi 
 cicNotationPres.cmi: mpresentation.cmi box.cmi 

diff --git a/helm/software/components/disambiguation/.depend b/helm/software/components/disambiguation/.depend
index aba9ffea7f8db60089a7cf1831da09dcf9d0c67d..9fdbeeeafa878cfe32dbf1f96adaad1e3044a4eb 100644 (file)
--- a/helm/software/components/disambiguation/.depend
+++ b/helm/software/components/disambiguation/.depend
@@ -1,3 +1,4 @@
+disambiguateTypes.cmi: 
 disambiguate.cmi: disambiguateTypes.cmi 
 multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi 
 disambiguateTypes.cmo: disambiguateTypes.cmi 

diff --git a/helm/software/components/disambiguation/.depend.opt b/helm/software/components/disambiguation/.depend.opt
index aba9ffea7f8db60089a7cf1831da09dcf9d0c67d..9fdbeeeafa878cfe32dbf1f96adaad1e3044a4eb 100644 (file)
--- a/helm/software/components/disambiguation/.depend.opt
+++ b/helm/software/components/disambiguation/.depend.opt
@@ -1,3 +1,4 @@
+disambiguateTypes.cmi: 
 disambiguate.cmi: disambiguateTypes.cmi 
 multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi 
 disambiguateTypes.cmo: disambiguateTypes.cmi 

diff --git a/helm/software/components/extlib/.depend b/helm/software/components/extlib/.depend
index 201cd0cba99efc82def4f425a72ba0e952c1a5ea..dcc6377a0664b620f19f47d8103c5b3a88a03270 100644 (file)
--- a/helm/software/components/extlib/.depend
+++ b/helm/software/components/extlib/.depend
@@ -1,3 +1,13 @@
+componentsConf.cmi: 
+hExtlib.cmi: 
+hMarshal.cmi: 
+patternMatcher.cmi: 
+hLog.cmi: 
+trie.cmi: 
+discrimination_tree.cmi: 
+hTopoSort.cmi: 
+refCounter.cmi: 
+graphvizPp.cmi: 
 componentsConf.cmo: componentsConf.cmi 
 componentsConf.cmx: componentsConf.cmi 
 hExtlib.cmo: hExtlib.cmi 

diff --git a/helm/software/components/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt
index 201cd0cba99efc82def4f425a72ba0e952c1a5ea..dcc6377a0664b620f19f47d8103c5b3a88a03270 100644 (file)
--- a/helm/software/components/extlib/.depend.opt
+++ b/helm/software/components/extlib/.depend.opt
@@ -1,3 +1,13 @@
+componentsConf.cmi: 
+hExtlib.cmi: 
+hMarshal.cmi: 
+patternMatcher.cmi: 
+hLog.cmi: 
+trie.cmi: 
+discrimination_tree.cmi: 
+hTopoSort.cmi: 
+refCounter.cmi: 
+graphvizPp.cmi: 
 componentsConf.cmo: componentsConf.cmi 
 componentsConf.cmx: componentsConf.cmi 
 hExtlib.cmo: hExtlib.cmi 

diff --git a/helm/software/components/getter/.depend b/helm/software/components/getter/.depend
index 20f69cf0c810c91e600fa5263c93c1b0ce86f3cb..ca64d8ec04f2c9e9b431d4921064c88bbb7587c9 100644 (file)
--- a/helm/software/components/getter/.depend
+++ b/helm/software/components/getter/.depend
@@ -1,6 +1,13 @@
+http_getter_wget.cmi: 
+http_getter_logger.cmi: 
+http_getter_misc.cmi: 
+http_getter_const.cmi: 
 http_getter_env.cmi: http_getter_types.cmo 
+http_getter_storage.cmi: 
 http_getter_common.cmi: http_getter_types.cmo 
 http_getter.cmi: http_getter_types.cmo 
+http_getter_types.cmo: 
+http_getter_types.cmx: 
 http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi 
 http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi 
 http_getter_logger.cmo: http_getter_logger.cmi 

diff --git a/helm/software/components/getter/.depend.opt b/helm/software/components/getter/.depend.opt
index 554fb1ec771351761436b91c8d3f77c3a389d95e..64da37f137deef8a5baebcbd07ba8f62cbf8e39c 100644 (file)
--- a/helm/software/components/getter/.depend.opt
+++ b/helm/software/components/getter/.depend.opt
@@ -1,6 +1,13 @@
+http_getter_wget.cmi: 
+http_getter_logger.cmi: 
+http_getter_misc.cmi: 
+http_getter_const.cmi: 
 http_getter_env.cmi: http_getter_types.cmx 
+http_getter_storage.cmi: 
 http_getter_common.cmi: http_getter_types.cmx 
 http_getter.cmi: http_getter_types.cmx 
+http_getter_types.cmo: 
+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 

diff --git a/helm/software/components/grafite/.depend b/helm/software/components/grafite/.depend
index dc225e2212dc37bb6eb22aa150fddf713965a312..f305b15803a9f6b7f87ab353a1e871afb8f6a1a5 100644 (file)
--- a/helm/software/components/grafite/.depend
+++ b/helm/software/components/grafite/.depend
@@ -1,5 +1,7 @@
 grafiteAstPp.cmi: grafiteAst.cmo 
 grafiteMarshal.cmi: grafiteAst.cmo 
+grafiteAst.cmo: 
+grafiteAst.cmx: 
 grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi 
 grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi 
 grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi 

diff --git a/helm/software/components/grafite/.depend.opt b/helm/software/components/grafite/.depend.opt
index 0f64ba7893909077481333c64a3c07fe5dc62349..e01d5bbfa69e67b34b9eaa941cf4a3c4351c174c 100644 (file)
--- a/helm/software/components/grafite/.depend.opt
+++ b/helm/software/components/grafite/.depend.opt
@@ -1,5 +1,7 @@
 grafiteAstPp.cmi: grafiteAst.cmx 
 grafiteMarshal.cmi: grafiteAst.cmx 
+grafiteAst.cmo: 
+grafiteAst.cmx: 
 grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi 
 grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi 
 grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi 

diff --git a/helm/software/components/grafite_engine/.depend b/helm/software/components/grafite_engine/.depend
index a545f14e33d0a91238cbcf0bd0a65c6eb18b1eae..10236823af172c045fb709552131af884aaf6872 100644 (file)
--- a/helm/software/components/grafite_engine/.depend
+++ b/helm/software/components/grafite_engine/.depend
@@ -1,3 +1,4 @@
+grafiteTypes.cmi: 
 grafiteSync.cmi: grafiteTypes.cmi 
 nCicCoercDeclaration.cmi: grafiteTypes.cmi 
 grafiteEngine.cmi: grafiteTypes.cmi 

diff --git a/helm/software/components/grafite_engine/.depend.opt b/helm/software/components/grafite_engine/.depend.opt
index a545f14e33d0a91238cbcf0bd0a65c6eb18b1eae..10236823af172c045fb709552131af884aaf6872 100644 (file)
--- a/helm/software/components/grafite_engine/.depend.opt
+++ b/helm/software/components/grafite_engine/.depend.opt
@@ -1,3 +1,4 @@
+grafiteTypes.cmi: 
 grafiteSync.cmi: grafiteTypes.cmi 
 nCicCoercDeclaration.cmi: grafiteTypes.cmi 
 grafiteEngine.cmi: grafiteTypes.cmi 

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 5ae6e92ed682981d179a29d5f1d9549d5dfc56f9..9fa8dbb000a30e17e20b5f221b142b5cf77db098 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -487,8 +487,10 @@ let inject_unification_hint =
  =
   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
  in
-  NCicLibrary.Serializer.register 
-    "unification_hints" basic_eval_unification_hint
+  NCicLibrary.Serializer.register#run "unification_hints"
+   object(_ : 'a NCicLibrary.register_type)
+     method run = basic_eval_unification_hint
+   end
 ;;
 
 let eval_unification_hint status t n = 
@@ -502,6 +504,45 @@ let eval_unification_hint status t n =
   status,`New []
 ;;
 
+let basic_index_obj l status =
+  status#set_auto_cache 
+    (List.fold_left
+      (fun t (k,v) -> 
+         NDiscriminationTree.DiscriminationTree.index t k v) 
+    status#auto_cache l) 
+;;     
+
+let record_index_obj = 
+ let aux l 
+   ~refresh_uri_in_universe 
+   ~refresh_uri_in_term
+ =
+    basic_index_obj
+      (List.map 
+        (fun k,v -> refresh_uri_in_term k, refresh_uri_in_term v) 
+      l)
+ in
+  NCicLibrary.Serializer.register#run "index_obj"
+   object(_ : 'a NCicLibrary.register_type)
+     method run = aux
+   end
+;;
+
+let index_obj_for_auto status (uri, height, _, _, kind) = 
+ let data = 
+  match kind with
+  | NCic.Fixpoint _ -> []
+  | NCic.Inductive _ -> []
+  | NCic.Constant (_,_,_, ty, _) ->
+      [ ty, NCic.Const(NReference.reference_of_spec 
+              uri (NReference.Def height)) ]
+ in
+ let status = basic_index_obj data status in
+ let dump = record_index_obj data :: status#dump in
+ status#set_dump dump
+;; 
+
+
 let basic_eval_add_constraint (u1,u2) status =
  NCicLibrary.add_constraint status u1 u2
 ;;
@@ -515,7 +556,10 @@ let inject_constraint =
   let u2 = refresh_uri_in_universe u2 in 
   basic_eval_add_constraint (u1,u2)
  in
-  NCicLibrary.Serializer.register "constraints" basic_eval_add_constraint
+  NCicLibrary.Serializer.register#run "constraints"
+   object(_:'a NCicLibrary.register_type)
+     method run = basic_eval_add_constraint 
+   end
 ;;
 
 let eval_add_constraint status u1 u2 = 
@@ -709,6 +753,7 @@ let subst_metasenv_and_fix_names status =
    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
 ;;
 
+
 let rec eval_ncommand opts status (text,prefix_len,cmd) =
   match cmd with
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
@@ -748,6 +793,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj = uri,height,[],[],obj_kind in
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
+        let status = index_obj_for_auto status obj in
 (*         prerr_endline (NCicPp.ppobj obj); *)
         HLog.message ("New object: " ^ NUri.string_of_uri uri);
          (try

diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
index 2f103cf83f944fe2255a908cf7c10779803b4da1..ea112bf4ebb16deb048be05402c2b91f2221b24d 100644 (file)
--- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml
@@ -294,7 +294,10 @@ let record_ncoercion =
  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
    List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
  in
-  NCicLibrary.Serializer.register "ncoercion" aux_l
+  NCicLibrary.Serializer.register#run "ncoercion"
+   object(self : 'a NCicLibrary.register_type)
+    method run = aux_l 
+   end
 ;;
 
 let basic_eval_and_record_ncoercion infos status =

diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend
index 97bf4d7c26591b45c8b7710b18ccc7b10bfce265..2766b04d03ad96eb26664ce893da8d732191ede5 100644 (file)
--- a/helm/software/components/grafite_parser/.depend
+++ b/helm/software/components/grafite_parser/.depend
@@ -1,4 +1,9 @@
+dependenciesParser.cmi: 
+grafiteParser.cmi: 
+cicNotation2.cmi: 
+nEstatus.cmi: 
 grafiteDisambiguate.cmi: nEstatus.cmi 
+print_grammar.cmi: 
 dependenciesParser.cmo: dependenciesParser.cmi 
 dependenciesParser.cmx: dependenciesParser.cmi 
 grafiteParser.cmo: grafiteParser.cmi 

diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt
index 97bf4d7c26591b45c8b7710b18ccc7b10bfce265..2766b04d03ad96eb26664ce893da8d732191ede5 100644 (file)
--- a/helm/software/components/grafite_parser/.depend.opt
+++ b/helm/software/components/grafite_parser/.depend.opt
@@ -1,4 +1,9 @@
+dependenciesParser.cmi: 
+grafiteParser.cmi: 
+cicNotation2.cmi: 
+nEstatus.cmi: 
 grafiteDisambiguate.cmi: nEstatus.cmi 
+print_grammar.cmi: 
 dependenciesParser.cmo: dependenciesParser.cmi 
 dependenciesParser.cmx: dependenciesParser.cmi 
 grafiteParser.cmo: grafiteParser.cmi 

diff --git a/helm/software/components/hgdome/.depend b/helm/software/components/hgdome/.depend
index bf9c09af77949af3443918acfe26309ababdde62..072d9697ac67fab4c4d0dffd6321082b1022c444 100644 (file)
--- a/helm/software/components/hgdome/.depend
+++ b/helm/software/components/hgdome/.depend
@@ -1,3 +1,5 @@
+domMisc.cmi: 
+xml2Gdome.cmi: 
 domMisc.cmo: domMisc.cmi 
 domMisc.cmx: domMisc.cmi 
 xml2Gdome.cmo: xml2Gdome.cmi 

diff --git a/helm/software/components/hgdome/.depend.opt b/helm/software/components/hgdome/.depend.opt
index bf9c09af77949af3443918acfe26309ababdde62..072d9697ac67fab4c4d0dffd6321082b1022c444 100644 (file)
--- a/helm/software/components/hgdome/.depend.opt
+++ b/helm/software/components/hgdome/.depend.opt
@@ -1,3 +1,5 @@
+domMisc.cmi: 
+xml2Gdome.cmi: 
 domMisc.cmo: domMisc.cmi 
 domMisc.cmx: domMisc.cmi 
 xml2Gdome.cmo: xml2Gdome.cmi 

diff --git a/helm/software/components/hmysql/.depend b/helm/software/components/hmysql/.depend
index 16e6e9da7ff478b574edcc5f5756da5ac302ed34..ce439d961c5806d62c02572a1790a6b6591aad1a 100644 (file)
--- a/helm/software/components/hmysql/.depend
+++ b/helm/software/components/hmysql/.depend
@@ -1,2 +1,7 @@
+hSql.cmi: 
+hSqlite3.cmo: 
+hSqlite3.cmx: 
+hMysql.cmo: 
+hMysql.cmx: 
 hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi 
 hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi 

diff --git a/helm/software/components/hmysql/.depend.opt b/helm/software/components/hmysql/.depend.opt
index 602c901b81f28e6d8f557a971cd84673bfb701c9..c2289bff28e2b3c806b7240252460a805274a528 100644 (file)
--- a/helm/software/components/hmysql/.depend.opt
+++ b/helm/software/components/hmysql/.depend.opt
@@ -1,2 +1,7 @@
+hSql.cmi: 
+hSqlite3.cmo: 
+hSqlite3.cmx: 
+hMysql.cmo: 
+hMysql.cmx: 
 hSql.cmo: hSqlite3.cmx hMysql.cmx hSql.cmi 
 hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi 

diff --git a/helm/software/components/lexicon/.depend b/helm/software/components/lexicon/.depend
index 847a4a807733e1ff71a24f44d6ff3ed18dd0252b..16c1145165e3acf1c2c923e16a634ce3f3967bef 100644 (file)
--- a/helm/software/components/lexicon/.depend
+++ b/helm/software/components/lexicon/.depend
@@ -3,6 +3,8 @@ lexiconMarshal.cmi: lexiconAst.cmo
 cicNotation.cmi: lexiconAst.cmo 
 lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi 
 lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo 
+lexiconAst.cmo: 
+lexiconAst.cmx: 
 lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi 
 lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi 
 lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi 

diff --git a/helm/software/components/lexicon/.depend.opt b/helm/software/components/lexicon/.depend.opt
index 463d8a7bc2ab55bca12b9ff9c3ecfbb4e7bf222b..0fee4b18e0ea1c8028d8a00805d03f848b06c55d 100644 (file)
--- a/helm/software/components/lexicon/.depend.opt
+++ b/helm/software/components/lexicon/.depend.opt
@@ -3,6 +3,8 @@ lexiconMarshal.cmi: lexiconAst.cmx
 cicNotation.cmi: lexiconAst.cmx 
 lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi 
 lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx 
+lexiconAst.cmo: 
+lexiconAst.cmx: 
 lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi 
 lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi 
 lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi 

diff --git a/helm/software/components/library/.depend b/helm/software/components/library/.depend
index a9f24f814f3dfb119e00e1fe2f6d71ef565d38ff..cfa1295edcd418319d423cb3ad3f4cc106a1ff21 100644 (file)
--- a/helm/software/components/library/.depend
+++ b/helm/software/components/library/.depend
@@ -1,4 +1,13 @@
+librarian.cmi: 
+libraryMisc.cmi: 
+libraryDb.cmi: 
+coercDb.cmi: 
 cicCoercion.cmi: coercDb.cmi 
+librarySync.cmi: 
+cicElim.cmi: 
+cicRecord.cmi: 
+cicFix.cmi: 
+libraryClean.cmi: 
 librarian.cmo: librarian.cmi 
 librarian.cmx: librarian.cmi 
 libraryMisc.cmo: libraryMisc.cmi 

diff --git a/helm/software/components/library/.depend.opt b/helm/software/components/library/.depend.opt
index a9f24f814f3dfb119e00e1fe2f6d71ef565d38ff..cfa1295edcd418319d423cb3ad3f4cc106a1ff21 100644 (file)
--- a/helm/software/components/library/.depend.opt
+++ b/helm/software/components/library/.depend.opt
@@ -1,4 +1,13 @@
+librarian.cmi: 
+libraryMisc.cmi: 
+libraryDb.cmi: 
+coercDb.cmi: 
 cicCoercion.cmi: coercDb.cmi 
+librarySync.cmi: 
+cicElim.cmi: 
+cicRecord.cmi: 
+cicFix.cmi: 
+libraryClean.cmi: 
 librarian.cmo: librarian.cmi 
 librarian.cmx: librarian.cmi 
 libraryMisc.cmo: libraryMisc.cmi 

diff --git a/helm/software/components/logger/.depend b/helm/software/components/logger/.depend
index 28268d29ee15cd05d86a0565b7d47abfe8ecf81f..dfb4400ff0dce00c92943043edccecc0c1222ed5 100644 (file)
--- a/helm/software/components/logger/.depend
+++ b/helm/software/components/logger/.depend
@@ -1,2 +1,3 @@
+helmLogger.cmi: 
 helmLogger.cmo: helmLogger.cmi 
 helmLogger.cmx: helmLogger.cmi 

diff --git a/helm/software/components/logger/.depend.opt b/helm/software/components/logger/.depend.opt
index 28268d29ee15cd05d86a0565b7d47abfe8ecf81f..dfb4400ff0dce00c92943043edccecc0c1222ed5 100644 (file)
--- a/helm/software/components/logger/.depend.opt
+++ b/helm/software/components/logger/.depend.opt
@@ -1,2 +1,3 @@
+helmLogger.cmi: 
 helmLogger.cmo: helmLogger.cmi 
 helmLogger.cmx: helmLogger.cmi 

diff --git a/helm/software/components/metadata/.depend b/helm/software/components/metadata/.depend
index 492a34e3a9dad11aa9a08d4a09802647c6e0bf95..78cd97a0deff8787b73aed2878acef8374029ee0 100644 (file)
--- a/helm/software/components/metadata/.depend
+++ b/helm/software/components/metadata/.depend
@@ -1,3 +1,5 @@
+sqlStatements.cmi: 
+metadataTypes.cmi: 
 metadataExtractor.cmi: metadataTypes.cmi 
 metadataPp.cmi: metadataTypes.cmi 
 metadataConstraints.cmi: metadataTypes.cmi 

diff --git a/helm/software/components/metadata/.depend.opt b/helm/software/components/metadata/.depend.opt
index 492a34e3a9dad11aa9a08d4a09802647c6e0bf95..78cd97a0deff8787b73aed2878acef8374029ee0 100644 (file)
--- a/helm/software/components/metadata/.depend.opt
+++ b/helm/software/components/metadata/.depend.opt
@@ -1,3 +1,5 @@
+sqlStatements.cmi: 
+metadataTypes.cmi: 
 metadataExtractor.cmi: metadataTypes.cmi 
 metadataPp.cmi: metadataTypes.cmi 
 metadataConstraints.cmi: metadataTypes.cmi 

diff --git a/helm/software/components/ng_cic_content/.depend b/helm/software/components/ng_cic_content/.depend
index b4e17fa99bca931a5289d06541f5b69060d11594..1316c8eab83e4c08ca7047ed72175492e98197a1 100644 (file)
--- a/helm/software/components/ng_cic_content/.depend
+++ b/helm/software/components/ng_cic_content/.depend
@@ -1,3 +1,5 @@
+ncic2astMatcher.cmi: 
+nTermCicContent.cmi: 
 ncic2astMatcher.cmo: ncic2astMatcher.cmi 
 ncic2astMatcher.cmx: ncic2astMatcher.cmi 
 nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi 

diff --git a/helm/software/components/ng_cic_content/.depend.opt b/helm/software/components/ng_cic_content/.depend.opt
index b4e17fa99bca931a5289d06541f5b69060d11594..1316c8eab83e4c08ca7047ed72175492e98197a1 100644 (file)
--- a/helm/software/components/ng_cic_content/.depend.opt
+++ b/helm/software/components/ng_cic_content/.depend.opt
@@ -1,3 +1,5 @@
+ncic2astMatcher.cmi: 
+nTermCicContent.cmi: 
 ncic2astMatcher.cmo: ncic2astMatcher.cmi 
 ncic2astMatcher.cmx: ncic2astMatcher.cmi 
 nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi 

diff --git a/helm/software/components/ng_disambiguation/.depend b/helm/software/components/ng_disambiguation/.depend
index 6b4ef95c1ee75472df6140057f1b06851033b996..2de54dc5eaedce21d8850cc5f76cc76f38331752 100644 (file)
--- a/helm/software/components/ng_disambiguation/.depend
+++ b/helm/software/components/ng_disambiguation/.depend
@@ -1,2 +1,3 @@
+nCicDisambiguate.cmi: 
 nCicDisambiguate.cmo: nCicDisambiguate.cmi 
 nCicDisambiguate.cmx: nCicDisambiguate.cmi 

diff --git a/helm/software/components/ng_disambiguation/.depend.opt b/helm/software/components/ng_disambiguation/.depend.opt
index 6b4ef95c1ee75472df6140057f1b06851033b996..2de54dc5eaedce21d8850cc5f76cc76f38331752 100644 (file)
--- a/helm/software/components/ng_disambiguation/.depend.opt
+++ b/helm/software/components/ng_disambiguation/.depend.opt
@@ -1,2 +1,3 @@
+nCicDisambiguate.cmi: 
 nCicDisambiguate.cmo: nCicDisambiguate.cmi 
 nCicDisambiguate.cmx: nCicDisambiguate.cmi 

diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index fa6e420640000afcb42a2dccf0d31ad985b402dc..365aaf26188695786deb73106de76b231a374f7a 100644 (file)
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -1,3 +1,4 @@
+nUri.cmi: 
 nReference.cmi: nUri.cmi 
 nCicUtils.cmi: nCic.cmo 
 nCicSubstitution.cmi: nCic.cmo 

diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt
index 7720472e833fdbe6a9d96e0670811d44990199fa..f50abe93cdac32eb8d3400fcf532927049707cbf 100644 (file)
--- a/helm/software/components/ng_kernel/.depend.opt
+++ b/helm/software/components/ng_kernel/.depend.opt
@@ -1,3 +1,4 @@
+nUri.cmi: 
 nReference.cmi: nUri.cmi 
 nCicUtils.cmi: nCic.cmx 
 nCicSubstitution.cmi: nCic.cmx 

diff --git a/helm/software/components/ng_library/.depend b/helm/software/components/ng_library/.depend
index c76001c01994219bd09ad475a79d0e3b20568227..48127a32524c5ddf62190d9f5127650cbf289c7c 100644 (file)
--- a/helm/software/components/ng_library/.depend
+++ b/helm/software/components/ng_library/.depend
@@ -1,2 +1,3 @@
+nCicLibrary.cmi: 
 nCicLibrary.cmo: nCicLibrary.cmi 
 nCicLibrary.cmx: nCicLibrary.cmi 

diff --git a/helm/software/components/ng_library/.depend.opt b/helm/software/components/ng_library/.depend.opt
index c76001c01994219bd09ad475a79d0e3b20568227..48127a32524c5ddf62190d9f5127650cbf289c7c 100644 (file)
--- a/helm/software/components/ng_library/.depend.opt
+++ b/helm/software/components/ng_library/.depend.opt
@@ -1,2 +1,3 @@
+nCicLibrary.cmi: 
 nCicLibrary.cmo: nCicLibrary.cmi 
 nCicLibrary.cmx: nCicLibrary.cmi 

diff --git a/helm/software/components/ng_library/nCicLibrary.ml b/helm/software/components/ng_library/nCicLibrary.ml
index 6987ec1aa698e8b9560854754acc22063947eb43..c5b43d7ca52eeb8b3f43db6bb5835c1d01949bbb 100644 (file)
--- a/helm/software/components/ng_library/nCicLibrary.ml
+++ b/helm/software/components/ng_library/nCicLibrary.ml
@@ -143,6 +143,23 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
+type automation_cache = NDiscriminationTree.DiscriminationTree.t
+
+class type g_auto_status =
+ object
+  method auto_cache : automation_cache
+ end
+
+class auto_status =
+ object(self)
+  val auto_cache = NDiscriminationTree.DiscriminationTree.empty
+  method auto_cache = auto_cache
+  method set_auto_cache v = {< auto_cache = v >}
+  method set_auto_status
+   : 'status. #g_auto_status as 'status -> 'self
+   = fun o -> self#set_auto_cache o#auto_cache
+ end
+
 class type g_status =
  object
   inherit NRstatus.g_status
@@ -150,27 +167,14 @@ class type g_status =
  end
 
 class status =
- object
+ object(self)
   inherit NRstatus.status
   val timestamp = (time0 : timestamp)
   method timestamp = timestamp
   method set_timestamp v = {< timestamp = v >}
   method set_library_status
    : 'status. #g_status as 'status -> 'self
-   = fun o -> {< timestamp = o#timestamp >}
- end
-
-
-module type SerializerT =
- sig
-  type status
-  type obj
-  val register:
-   string ->
-    ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
-    ('a -> obj)
-  val serialize: baseuri:NUri.uri -> obj list -> unit
-  val require: baseuri:NUri.uri -> status -> status
+   = fun o -> self#set_timestamp o#timestamp
  end
 
 let time_travel status =
@@ -198,65 +202,66 @@ let serialize ~baseuri dump =
  List.iter (fun u -> add_deps u [baseuri]) !includes;
  time_travel (new status)
 ;;
+  
+type obj = string * Obj.t
 
-module SerializerF(S: sig type status end) =
- struct
-  type status = S.status
-  type obj = string * Obj.t
-
-  let require1 = ref (fun _ -> assert false (* unknown data*))
-  let already_registered = ref []
-
-  let register tag require =
-   assert (not (List.mem tag !already_registered));
-   already_registered := tag :: !already_registered;
-   let old_require1 = !require1 in
-   require1 :=
-     (fun (tag',data) as x ->
-      if tag=tag' then
-       require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term 
-      else
-       old_require1 x);
-   (fun x -> tag,Obj.repr x)
-
-  let serialize = serialize
-
-  let require ~baseuri status =
-   includes := baseuri::!includes;
-   let dump = require0 ~baseuri in
-    List.fold_right !require1 dump status
-end
-
-type sstatus = status
-
-module Serializer =
- struct
-  include SerializerF(struct type status = sstatus end)
-
-  let require ~baseuri status = 
-   let rstatus = require ~baseuri (status : #status :> status) in
-   let status = status#set_coerc_db (rstatus#coerc_db) in
-   let status = status#set_uhint_db (rstatus#uhint_db) in
-   let status = status#set_timestamp (rstatus#timestamp) in
-    status 
- end
 
 class type g_dumpable_status =
  object
   inherit g_status
-  method dump: Serializer.obj list
+  inherit g_auto_status
+  method dump: obj list
  end
 
 class dumpable_status =
  object(self)
   inherit status
-  val dump = ([] : Serializer.obj list)
+  inherit auto_status
+  val dump = ([] : obj list)
   method dump = dump
   method set_dump v = {< dump = v >}
   method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self
-   = fun o -> (self#set_dump o#dump)#set_coercion_status o
+   = fun o -> ((self#set_dump o#dump)#set_coercion_status o)#set_auto_status o
  end
 
+type 'a register_type =
+ < run: 'status.
+    'a -> refresh_uri_in_universe:(NCic.universe ->
+      NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) ->
+       (#dumpable_status as 'status) -> 'status >
+
+module Serializer =
+ struct
+  let require1 = ref (object method run : 'status. obj -> (#dumpable_status as 'status) -> 'status  = fun _ -> assert false end (* unknown data*))
+  let already_registered = ref []
+
+  let register =
+   object
+    method run : 'a.  string -> 'a register_type -> ('a -> obj)
+    = fun tag require ->
+     assert (not (List.mem tag !already_registered));
+     already_registered := tag :: !already_registered;
+     let old_require1 = !require1 in
+     require1 :=
+       object
+        method run : 'status. obj -> (#dumpable_status as 'status) -> 'status =
+         fun ((tag',data) as x) ->
+         if tag=tag' then
+          require#run (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
+         else
+          old_require1#run x
+       end;
+     (fun x -> tag,Obj.repr x)
+   end
+
+  let serialize = serialize
+
+  let require ~baseuri status =
+   includes := baseuri::!includes;
+   let dump = require0 ~baseuri in
+    List.fold_right !require1#run dump status
+end
+
 
 let decompile ~baseuri =
  let baseuris = get_deps baseuri in

diff --git a/helm/software/components/ng_library/nCicLibrary.mli b/helm/software/components/ng_library/nCicLibrary.mli
index e155aaf4a3526e043f8d07a2e9562f7ed01cc492..ea1cfd4e523cc008de445256b1c9866156d20128 100644 (file)
--- a/helm/software/components/ng_library/nCicLibrary.mli
+++ b/helm/software/components/ng_library/nCicLibrary.mli
@@ -13,6 +13,20 @@
 
 exception LibraryOutOfSync of string Lazy.t
 
+type automation_cache = NDiscriminationTree.DiscriminationTree.t
+
+class type g_auto_status =
+ object
+  method auto_cache : automation_cache
+ end
+
+class auto_status :
+ object('self)
+  inherit g_auto_status
+  method set_auto_cache: automation_cache -> 'self
+  method set_auto_status: #g_auto_status -> 'self
+ end
+
 type timestamp
 
 class type g_status =
@@ -42,40 +56,39 @@ val clear_cache : unit -> unit
 val time_travel: #status -> unit
 val decompile: baseuri:NUri.uri -> unit
 
-module type SerializerT =
- sig
-  type status
-  type obj
-  val register:
-   string ->
-    ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
-    ('a -> obj)
-  val serialize: baseuri:NUri.uri -> obj list -> unit
-  val require: baseuri:NUri.uri -> status -> status
- end
-
 val init: unit -> unit
 
-module Serializer:
- sig
-  include SerializerT with type status = status 
-  val require: baseuri:NUri.uri -> (#status as 'status) -> 'status
- end
+type obj
 
 class type g_dumpable_status =
  object
   inherit g_status
-  method dump: Serializer.obj list
+  inherit g_auto_status
+  method dump: obj list
  end
-
+  
 class dumpable_status :
  object ('self)
   inherit status
+  inherit auto_status
   inherit g_dumpable_status
-  method set_dump: Serializer.obj list -> 'self
+  method set_dump: obj list -> 'self
   method set_dumpable_status: #g_dumpable_status -> 'self
  end
 
+type 'a register_type =
+ < run: 'status.
+    'a -> refresh_uri_in_universe:(NCic.universe ->
+      NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) ->
+       (#dumpable_status as 'status) -> 'status >
+
+module Serializer:
+ sig
+  val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >
+  val serialize: baseuri:NUri.uri -> obj list -> unit
+  val require: baseuri:NUri.uri -> (#dumpable_status as 'status) -> 'status
+ end
+
 (* CSC: only required during old-to-NG phase, to be deleted *)
 val refresh_uri: NUri.uri -> NUri.uri
 

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index 3ace5101400f920267785840a298257e8a1a2078..369ed6b69068acbe0644b42cf2d38e8f5bb48c02 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -1,3 +1,4 @@
+terms.cmi: 
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
@@ -10,6 +11,7 @@ paramod.cmi: terms.cmi orderings.cmi
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
 nCicProof.cmi: terms.cmi 
+nCicParamod.cmi: 
 terms.cmo: terms.cmi 
 terms.cmx: terms.cmi 
 pp.cmo: terms.cmi pp.cmi 

diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt
index 3ace5101400f920267785840a298257e8a1a2078..369ed6b69068acbe0644b42cf2d38e8f5bb48c02 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend.opt
+++ b/helm/software/components/ng_paramodulation/.depend.opt
@@ -1,3 +1,4 @@
+terms.cmi: 
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
@@ -10,6 +11,7 @@ paramod.cmi: terms.cmi orderings.cmi
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
 nCicProof.cmi: terms.cmi 
+nCicParamod.cmi: 
 terms.cmo: terms.cmi 
 terms.cmx: terms.cmi 
 pp.cmo: terms.cmi pp.cmi 

diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend
index f30b906fd908a88f33150931a8bd8e0d5d232e35..db7e5288428cc5c63f47f29ba31c99d41f9412d3 100644 (file)
--- a/helm/software/components/ng_refiner/.depend
+++ b/helm/software/components/ng_refiner/.depend
@@ -1,3 +1,6 @@
+nDiscriminationTree.cmi: 
+nCicMetaSubst.cmi: 
+nCicUnifHint.cmi: 
 nCicCoercion.cmi: nCicUnifHint.cmi 
 nRstatus.cmi: nCicCoercion.cmi 
 nCicUnification.cmi: nRstatus.cmi 

diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt
index f30b906fd908a88f33150931a8bd8e0d5d232e35..db7e5288428cc5c63f47f29ba31c99d41f9412d3 100644 (file)
--- a/helm/software/components/ng_refiner/.depend.opt
+++ b/helm/software/components/ng_refiner/.depend.opt
@@ -1,3 +1,6 @@
+nDiscriminationTree.cmi: 
+nCicMetaSubst.cmi: 
+nCicUnifHint.cmi: 
 nCicCoercion.cmi: nCicUnifHint.cmi 
 nRstatus.cmi: nCicCoercion.cmi 
 nCicUnification.cmi: nRstatus.cmi 

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 86ae2b375fcbbbc274d2917d6254aec5d68b5b58..7a49c201b82ace4e34fbc67990d96894c7d68b94 100644 (file)
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,3 +1,6 @@
+nCicTacReduction.cmi: 
+nTacStatus.cmi: 
+nCicElim.cmi: 
 nTactics.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 

diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt
index 86ae2b375fcbbbc274d2917d6254aec5d68b5b58..7a49c201b82ace4e34fbc67990d96894c7d68b94 100644 (file)
--- a/helm/software/components/ng_tactics/.depend.opt
+++ b/helm/software/components/ng_tactics/.depend.opt
@@ -1,3 +1,6 @@
+nCicTacReduction.cmi: 
+nTacStatus.cmi: 
+nCicElim.cmi: 
 nTactics.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 

diff --git a/helm/software/components/registry/.depend b/helm/software/components/registry/.depend
index cf4f36b68f502fc728be91d4b20e8b0dcd3658f2..40c03891a7433c13e27e38dbe1cb51e06030c905 100644 (file)
--- a/helm/software/components/registry/.depend
+++ b/helm/software/components/registry/.depend
@@ -1,2 +1,3 @@
+helm_registry.cmi: 
 helm_registry.cmo: helm_registry.cmi 
 helm_registry.cmx: helm_registry.cmi 

diff --git a/helm/software/components/registry/.depend.opt b/helm/software/components/registry/.depend.opt
index cf4f36b68f502fc728be91d4b20e8b0dcd3658f2..40c03891a7433c13e27e38dbe1cb51e06030c905 100644 (file)
--- a/helm/software/components/registry/.depend.opt
+++ b/helm/software/components/registry/.depend.opt
@@ -1,2 +1,3 @@
+helm_registry.cmi: 
 helm_registry.cmo: helm_registry.cmi 
 helm_registry.cmx: helm_registry.cmi 

diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend
index f3c6a8bd17a7351e99ce8e59905fda76a37cbf08..25e67131fca0487c4390d310d8307722b5058067 100644 (file)
--- a/helm/software/components/syntax_extensions/.depend
+++ b/helm/software/components/syntax_extensions/.depend
@@ -1,2 +1,5 @@
+utf8Macro.cmi: 
+utf8MacroTable.cmo: 
+utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 

diff --git a/helm/software/components/syntax_extensions/.depend.opt b/helm/software/components/syntax_extensions/.depend.opt
index c0cd9c9069420ca3c124fdf3a0f152838c5d121e..3d7dfc21fef76318d2516be6b5736428108d2d02 100644 (file)
--- a/helm/software/components/syntax_extensions/.depend.opt
+++ b/helm/software/components/syntax_extensions/.depend.opt
@@ -1,2 +1,5 @@
+utf8Macro.cmi: 
+utf8MacroTable.cmo: 
+utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 

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

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

diff --git a/helm/software/components/thread/.depend b/helm/software/components/thread/.depend
index 7759190c66cdd57bcc79c0da85a571cd76faa730..6616a03d0f4c0803fa1e9c2e309bbf89270e7526 100644 (file)
--- a/helm/software/components/thread/.depend
+++ b/helm/software/components/thread/.depend
@@ -1,3 +1,5 @@
+threadSafe.cmi: 
+extThread.cmi: 
 threadSafe.cmo: threadSafe.cmi 
 threadSafe.cmx: threadSafe.cmi 
 extThread.cmo: extThread.cmi 

diff --git a/helm/software/components/thread/.depend.opt b/helm/software/components/thread/.depend.opt
index 7759190c66cdd57bcc79c0da85a571cd76faa730..6616a03d0f4c0803fa1e9c2e309bbf89270e7526 100644 (file)
--- a/helm/software/components/thread/.depend.opt
+++ b/helm/software/components/thread/.depend.opt
@@ -1,3 +1,5 @@
+threadSafe.cmi: 
+extThread.cmi: 
 threadSafe.cmo: threadSafe.cmi 
 threadSafe.cmx: threadSafe.cmi 
 extThread.cmo: extThread.cmi 

diff --git a/helm/software/components/tptp_grafite/.depend b/helm/software/components/tptp_grafite/.depend
index bc310327f83551dd5875e62bfa3899e7c55559a2..a8972f4cfc20c049020440e4f567cfb622de8243 100644 (file)
--- a/helm/software/components/tptp_grafite/.depend
+++ b/helm/software/components/tptp_grafite/.depend
@@ -1,4 +1,7 @@
 parser.cmi: ast.cmo 
+tptp2grafite.cmi: 
+ast.cmo: 
+ast.cmx: 
 lexer.cmo: parser.cmi 
 lexer.cmx: parser.cmx 
 parser.cmo: ast.cmo parser.cmi 

diff --git a/helm/software/components/tptp_grafite/.depend.opt b/helm/software/components/tptp_grafite/.depend.opt
index c74300207fb532cff81cbdcd6146f285a05a7599..fb60fe8f2d6ae59e0b1b46ae5675794888fd335f 100644 (file)
--- a/helm/software/components/tptp_grafite/.depend.opt
+++ b/helm/software/components/tptp_grafite/.depend.opt
@@ -1,4 +1,7 @@
 parser.cmi: ast.cmx 
+tptp2grafite.cmi: 
+ast.cmo: 
+ast.cmx: 
 lexer.cmo: parser.cmi 
 lexer.cmx: parser.cmx 
 parser.cmo: ast.cmx parser.cmi 

diff --git a/helm/software/components/urimanager/.depend b/helm/software/components/urimanager/.depend
index 4821484239ac15df403da8d9123671544b3aa65f..9cac9aa783c7c003e70e118017c77b20d2ccb61a 100644 (file)
--- a/helm/software/components/urimanager/.depend
+++ b/helm/software/components/urimanager/.depend
@@ -1,2 +1,3 @@
+uriManager.cmi: 
 uriManager.cmo: uriManager.cmi 
 uriManager.cmx: uriManager.cmi 

diff --git a/helm/software/components/urimanager/.depend.opt b/helm/software/components/urimanager/.depend.opt
index 4821484239ac15df403da8d9123671544b3aa65f..9cac9aa783c7c003e70e118017c77b20d2ccb61a 100644 (file)
--- a/helm/software/components/urimanager/.depend.opt
+++ b/helm/software/components/urimanager/.depend.opt
@@ -1,2 +1,3 @@
+uriManager.cmi: 
 uriManager.cmo: uriManager.cmi 
 uriManager.cmx: uriManager.cmi 

diff --git a/helm/software/components/whelp/.depend b/helm/software/components/whelp/.depend
index 39f37dfa90077f1212c1f51f57ef8c55a21174c7..65dc079553f6476748ecdb106d61534fa746d753 100644 (file)
--- a/helm/software/components/whelp/.depend
+++ b/helm/software/components/whelp/.depend
@@ -1,3 +1,5 @@
+whelp.cmi: 
+fwdQueries.cmi: 
 whelp.cmo: whelp.cmi 
 whelp.cmx: whelp.cmi 
 fwdQueries.cmo: fwdQueries.cmi 

diff --git a/helm/software/components/whelp/.depend.opt b/helm/software/components/whelp/.depend.opt
index 39f37dfa90077f1212c1f51f57ef8c55a21174c7..65dc079553f6476748ecdb106d61534fa746d753 100644 (file)
--- a/helm/software/components/whelp/.depend.opt
+++ b/helm/software/components/whelp/.depend.opt
@@ -1,3 +1,5 @@
+whelp.cmi: 
+fwdQueries.cmi: 
 whelp.cmo: whelp.cmi 
 whelp.cmx: whelp.cmi 
 fwdQueries.cmo: fwdQueries.cmi 

diff --git a/helm/software/components/xml/.depend b/helm/software/components/xml/.depend
index 5ef59bdc96d40e0a64e0f50d91b949382a7f57e0..e7e7ffbd729fcdbc6206eb38afebf53940878718 100644 (file)
--- a/helm/software/components/xml/.depend
+++ b/helm/software/components/xml/.depend
@@ -1,3 +1,5 @@
+xml.cmi: 
+xmlPushParser.cmi: 
 xml.cmo: xml.cmi 
 xml.cmx: xml.cmi 
 xmlPushParser.cmo: xmlPushParser.cmi 

diff --git a/helm/software/components/xml/.depend.opt b/helm/software/components/xml/.depend.opt
index 5ef59bdc96d40e0a64e0f50d91b949382a7f57e0..e7e7ffbd729fcdbc6206eb38afebf53940878718 100644 (file)
--- a/helm/software/components/xml/.depend.opt
+++ b/helm/software/components/xml/.depend.opt
@@ -1,3 +1,5 @@
+xml.cmi: 
+xmlPushParser.cmi: 
 xml.cmo: xml.cmi 
 xml.cmx: xml.cmi 
 xmlPushParser.cmo: xmlPushParser.cmi 

diff --git a/helm/software/components/xmldiff/.depend b/helm/software/components/xmldiff/.depend
index e2832de332dd83fb5bd4beb1cd2b1e735d6fe35e..65bd7b9496155f928775a264636cae0249c62a98 100644 (file)
--- a/helm/software/components/xmldiff/.depend
+++ b/helm/software/components/xmldiff/.depend
@@ -1,2 +1,3 @@
+xmlDiff.cmi: 
 xmlDiff.cmo: xmlDiff.cmi 
 xmlDiff.cmx: xmlDiff.cmi 

diff --git a/helm/software/components/xmldiff/.depend.opt b/helm/software/components/xmldiff/.depend.opt
index e2832de332dd83fb5bd4beb1cd2b1e735d6fe35e..65bd7b9496155f928775a264636cae0249c62a98 100644 (file)
--- a/helm/software/components/xmldiff/.depend.opt
+++ b/helm/software/components/xmldiff/.depend.opt
@@ -1,2 +1,3 @@
+xmlDiff.cmi: 
 xmlDiff.cmo: xmlDiff.cmi 
 xmlDiff.cmx: xmlDiff.cmi