Updated command ninverter. Syntax:

ninverter <id> for <indty> [<selection>] [: <target_sort>]

It is the same as the previous inverter except that:

- <selection> is now optional (when it is omitted, every index is selected)
- the user is allowed to specify a <target_sort> (when it is omitted, ninverter
  defaults to Prop, as it was the case for inverter)

diff --git a/helm/software/components/acic_content/.depend b/helm/software/components/acic_content/.depend
index 89dca0e446d48d1f05a1cda5fc3c39f1095257e3..8ade458af771b340426f4e4606d92e511c459a56 100644 (file)
--- a/helm/software/components/acic_content/.depend
+++ b/helm/software/components/acic_content/.depend
@@ -1,4 +1,3 @@
-content.cmi: 
 acic2content.cmi: content.cmi 
 content2cic.cmi: content.cmi 
 cicNotationUtil.cmi: cicNotationPt.cmo 
@@ -6,8 +5,6 @@ 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 307fceaa0288ab3dec50b1407588d9cb67d84bb5..fef8792567075850eb766452dd005034b8a354f9 100644 (file)
--- a/helm/software/components/acic_content/.depend.opt
+++ b/helm/software/components/acic_content/.depend.opt
@@ -1,4 +1,3 @@
-content.cmi: 
 acic2content.cmi: content.cmi 
 content2cic.cmi: content.cmi 
 cicNotationUtil.cmi: cicNotationPt.cmx 
@@ -6,8 +5,6 @@ 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 97238c4d861fc8ee80cbafc6c9c6337d3e3babf2..8d0128744c8b9e740462a1a8001764036199a67e 100644 (file)
--- a/helm/software/components/acic_procedural/.depend
+++ b/helm/software/components/acic_procedural/.depend
@@ -1,13 +1,6 @@
-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 97238c4d861fc8ee80cbafc6c9c6337d3e3babf2..8d0128744c8b9e740462a1a8001764036199a67e 100644 (file)
--- a/helm/software/components/acic_procedural/.depend.opt
+++ b/helm/software/components/acic_procedural/.depend.opt
@@ -1,13 +1,6 @@
-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 0c39328ae147e8ab714b2d3a7b1582a011b2b1d6..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/software/components/binaries/extractor/.depend
+++ b/helm/software/components/binaries/extractor/.depend
@@ -1,4 +0,0 @@
-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 0c39328ae147e8ab714b2d3a7b1582a011b2b1d6..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/software/components/binaries/extractor/.depend.opt
+++ b/helm/software/components/binaries/extractor/.depend.opt
@@ -1,4 +0,0 @@
-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 33147b94948d28fc9c7132773964d2547472c2ba..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/software/components/binaries/table_creator/.depend
+++ b/helm/software/components/binaries/table_creator/.depend
@@ -1,2 +0,0 @@
-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 33147b94948d28fc9c7132773964d2547472c2ba..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/software/components/binaries/table_creator/.depend.opt
+++ b/helm/software/components/binaries/table_creator/.depend.opt
@@ -1,2 +0,0 @@
-table_creator.cmo: 
-table_creator.cmx: 

diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend
index a835b247f3b3006e53a73a62b9ff56d394eca590..c2c7105c727f1c8101a1a119d3521629984d3dcf 100644 (file)
--- a/helm/software/components/cic/.depend
+++ b/helm/software/components/cic/.depend
@@ -1,10 +1,8 @@
-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 8cdd2a86aa5532872a81f4bf977cb65500389620..76d19c1ff002243a04033cccc16ff71f291e5167 100644 (file)
--- a/helm/software/components/cic/.depend.opt
+++ b/helm/software/components/cic/.depend.opt
@@ -1,10 +1,8 @@
-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 5449d50aaa2d43c1a8126f0561177e904f0975da..3fc1e0dce9eedda1f0bb74a669ad175582f03e06 100644 (file)
--- a/helm/software/components/cic_acic/.depend
+++ b/helm/software/components/cic_acic/.depend
@@ -1,6 +1,3 @@
-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 5449d50aaa2d43c1a8126f0561177e904f0975da..3fc1e0dce9eedda1f0bb74a669ad175582f03e06 100644 (file)
--- a/helm/software/components/cic_acic/.depend.opt
+++ b/helm/software/components/cic_acic/.depend.opt
@@ -1,6 +1,3 @@
-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 a9ae65a5e3c4c3df2f8aaca3b2762c794bee6bd5..e9bd1168f73e4e834b02480bca0e67e381fc4997 100644 (file)
--- a/helm/software/components/cic_disambiguation/.depend
+++ b/helm/software/components/cic_disambiguation/.depend
@@ -1,5 +1,3 @@
-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 a9ae65a5e3c4c3df2f8aaca3b2762c794bee6bd5..e9bd1168f73e4e834b02480bca0e67e381fc4997 100644 (file)
--- a/helm/software/components/cic_disambiguation/.depend.opt
+++ b/helm/software/components/cic_disambiguation/.depend.opt
@@ -1,5 +1,3 @@
-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 91be8d88d36bf6f3df5cd920db6a75f80a5ff64d..288ea5f6cf50f1cb6bb8ff00d53a0262825c3459 100644 (file)
--- a/helm/software/components/cic_exportation/.depend
+++ b/helm/software/components/cic_exportation/.depend
@@ -1,3 +1,2 @@
-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 91be8d88d36bf6f3df5cd920db6a75f80a5ff64d..288ea5f6cf50f1cb6bb8ff00d53a0262825c3459 100644 (file)
--- a/helm/software/components/cic_exportation/.depend.opt
+++ b/helm/software/components/cic_exportation/.depend.opt
@@ -1,3 +1,2 @@
-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 f8a16629ebd091a0c9e60b948c7e2eedb8908a16..5d83fd0f3d146e2d80ead2d8eb5c34b162a5835f 100644 (file)
--- a/helm/software/components/cic_proof_checking/.depend
+++ b/helm/software/components/cic_proof_checking/.depend
@@ -1,13 +1,3 @@
-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 f8a16629ebd091a0c9e60b948c7e2eedb8908a16..5d83fd0f3d146e2d80ead2d8eb5c34b162a5835f 100644 (file)
--- a/helm/software/components/cic_proof_checking/.depend.opt
+++ b/helm/software/components/cic_proof_checking/.depend.opt
@@ -1,13 +1,3 @@
-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 2e054f73d4e69376cc89138609538274bd8fe6d8..a7b23ceb4e8ba6ae3fdc2fa8352ce69acbde78b0 100644 (file)
--- a/helm/software/components/cic_unification/.depend
+++ b/helm/software/components/cic_unification/.depend
@@ -1,10 +1,3 @@
-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 2e054f73d4e69376cc89138609538274bd8fe6d8..a7b23ceb4e8ba6ae3fdc2fa8352ce69acbde78b0 100644 (file)
--- a/helm/software/components/cic_unification/.depend.opt
+++ b/helm/software/components/cic_unification/.depend.opt
@@ -1,10 +1,3 @@
-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 8d74439eb72834455b6f06006f1f5534312a3a51..6dd0e78a19212937b664b03fb796d8aaf496dbbb 100644 (file)
--- a/helm/software/components/content_pres/.depend
+++ b/helm/software/components/content_pres/.depend
@@ -1,9 +1,3 @@
-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 8d74439eb72834455b6f06006f1f5534312a3a51..6dd0e78a19212937b664b03fb796d8aaf496dbbb 100644 (file)
--- a/helm/software/components/content_pres/.depend.opt
+++ b/helm/software/components/content_pres/.depend.opt
@@ -1,9 +1,3 @@
-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 9fdbeeeafa878cfe32dbf1f96adaad1e3044a4eb..aba9ffea7f8db60089a7cf1831da09dcf9d0c67d 100644 (file)
--- a/helm/software/components/disambiguation/.depend
+++ b/helm/software/components/disambiguation/.depend
@@ -1,4 +1,3 @@
-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 9fdbeeeafa878cfe32dbf1f96adaad1e3044a4eb..aba9ffea7f8db60089a7cf1831da09dcf9d0c67d 100644 (file)
--- a/helm/software/components/disambiguation/.depend.opt
+++ b/helm/software/components/disambiguation/.depend.opt
@@ -1,4 +1,3 @@
-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 dcc6377a0664b620f19f47d8103c5b3a88a03270..201cd0cba99efc82def4f425a72ba0e952c1a5ea 100644 (file)
--- a/helm/software/components/extlib/.depend
+++ b/helm/software/components/extlib/.depend
@@ -1,13 +1,3 @@
-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 dcc6377a0664b620f19f47d8103c5b3a88a03270..201cd0cba99efc82def4f425a72ba0e952c1a5ea 100644 (file)
--- a/helm/software/components/extlib/.depend.opt
+++ b/helm/software/components/extlib/.depend.opt
@@ -1,13 +1,3 @@
-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 ca64d8ec04f2c9e9b431d4921064c88bbb7587c9..20f69cf0c810c91e600fa5263c93c1b0ce86f3cb 100644 (file)
--- a/helm/software/components/getter/.depend
+++ b/helm/software/components/getter/.depend
@@ -1,13 +1,6 @@
-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 64da37f137deef8a5baebcbd07ba8f62cbf8e39c..554fb1ec771351761436b91c8d3f77c3a389d95e 100644 (file)
--- a/helm/software/components/getter/.depend.opt
+++ b/helm/software/components/getter/.depend.opt
@@ -1,13 +1,6 @@
-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 f305b15803a9f6b7f87ab353a1e871afb8f6a1a5..dc225e2212dc37bb6eb22aa150fddf713965a312 100644 (file)
--- a/helm/software/components/grafite/.depend
+++ b/helm/software/components/grafite/.depend
@@ -1,7 +1,5 @@
 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 e01d5bbfa69e67b34b9eaa941cf4a3c4351c174c..0f64ba7893909077481333c64a3c07fe5dc62349 100644 (file)
--- a/helm/software/components/grafite/.depend.opt
+++ b/helm/software/components/grafite/.depend.opt
@@ -1,7 +1,5 @@
 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/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 86e657b6b5fe15eea32be64c15eda1fd5333ff03..0cfdef148ced4dfbae84f8d5f0199516cc86e7a3 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -220,7 +220,7 @@ type ('term,'obj) command =
 type ncommand =
   | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
   | NObj of loc * CicNotationPt.term CicNotationPt.obj
-  | NInverter of loc * string * CicNotationPt.term
+  | NInverter of loc * string * CicNotationPt.term * bool list option * CicNotationPt.term option
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string *

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 8cb7538ba2ad84dc4b322a3d979f0c2f406d4327..83f3a36b6f7a37000c20de0a2996b6a784966e0c 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -371,7 +371,7 @@ let pp_coercion ~term_pp t do_composites arity saturations=
 let pp_ncommand = function
   | UnificationHint (_,t, n) -> 
       "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
-  | NInverter (_,_,_)
+  | NInverter (_,_,_,_,_)
   | NObj (_,_)
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"

diff --git a/helm/software/components/grafite_engine/.depend b/helm/software/components/grafite_engine/.depend
index 10236823af172c045fb709552131af884aaf6872..a545f14e33d0a91238cbcf0bd0a65c6eb18b1eae 100644 (file)
--- a/helm/software/components/grafite_engine/.depend
+++ b/helm/software/components/grafite_engine/.depend
@@ -1,4 +1,3 @@
-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 10236823af172c045fb709552131af884aaf6872..a545f14e33d0a91238cbcf0bd0a65c6eb18b1eae 100644 (file)
--- a/helm/software/components/grafite_engine/.depend.opt
+++ b/helm/software/components/grafite_engine/.depend.opt
@@ -1,4 +1,3 @@
-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 0806057ec14ab1d67189dba4832028c6509576db..494701d2d30a63a62519de80755a82d0780344e2 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -861,22 +861,32 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
-  | GrafiteAst.NInverter (loc, name, indty) ->
+  | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
      else
+      let metasenv,subst,status,sort = match sort with
+        | None -> [],[],status,NCic.Sort NCic.Prop
+        | Some s -> GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                      (text,prefix_len,s) 
+      in
+      assert (metasenv = []);
+      let sort = NCicReduction.whd ~subst [] sort in
+      let sort = match sort with 
+          NCic.Sort s -> s
+        | _ ->  raise (Invalid_argument (Printf.sprintf "ninverter: found target %s, which is not a sort" 
+                                           (NCicPp.ppterm ~metasenv ~subst ~context:[] sort)))
+      in
       let status = status#set_ng_mode `ProofMode in
       let metasenv,subst,status,indty =
-       GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
-      let _,leftno,tys,_,_ = match indty with
-          NCic.Const r -> NCicEnvironment.get_checked_indtys r
-        | _ -> assert false in
-      let it = match tys with
-          hd::tl -> hd
-        | _ -> assert false
-      in
-     let status,obj =
-      NInversion.mk_inverter name it leftno status status#baseuri in
+       GrafiteDisambiguate.disambiguate_nterm None status [] [] subst (text,prefix_len,indty) in
+      let indtyno,(_,leftno,tys,_,_) = match indty with
+          NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) -> 
+            indtyno, NCicEnvironment.get_checked_indtys r
+        | _ -> prerr_endline ("engine: indty ="  ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in
+      let it = List.nth tys indtyno in
+     let status,obj = NInversion.mk_inverter name it leftno ?selection sort 
+                        status status#baseuri in
      let _,_,menv,_,_ = obj in
      (match menv with
         [] ->

diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend
index 2766b04d03ad96eb26664ce893da8d732191ede5..97bf4d7c26591b45c8b7710b18ccc7b10bfce265 100644 (file)
--- a/helm/software/components/grafite_parser/.depend
+++ b/helm/software/components/grafite_parser/.depend
@@ -1,9 +1,4 @@
-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 2766b04d03ad96eb26664ce893da8d732191ede5..97bf4d7c26591b45c8b7710b18ccc7b10bfce265 100644 (file)
--- a/helm/software/components/grafite_parser/.depend.opt
+++ b/helm/software/components/grafite_parser/.depend.opt
@@ -1,9 +1,4 @@
-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/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 8a418200d94604127cd7aad3a000aafdca921417..2fbfe41790e77e0b3c8328fe38df2099bcd10c70 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -803,8 +803,10 @@ EXTEND
         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
-    | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = term -> 
-        G.NInverter (loc,name,indty)
+    | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
+      paramspec = OPT inverter_param_list ; 
+      outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
+        G.NInverter (loc,name,indty,paramspec,outsort)
     | NLETCOREC ; defs = let_defs -> 
         nmk_rec_corec `CoInductive defs loc
     | NLETREC ; defs = let_defs -> 

diff --git a/helm/software/components/hgdome/.depend b/helm/software/components/hgdome/.depend
index 072d9697ac67fab4c4d0dffd6321082b1022c444..bf9c09af77949af3443918acfe26309ababdde62 100644 (file)
--- a/helm/software/components/hgdome/.depend
+++ b/helm/software/components/hgdome/.depend
@@ -1,5 +1,3 @@
-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 072d9697ac67fab4c4d0dffd6321082b1022c444..bf9c09af77949af3443918acfe26309ababdde62 100644 (file)
--- a/helm/software/components/hgdome/.depend.opt
+++ b/helm/software/components/hgdome/.depend.opt
@@ -1,5 +1,3 @@
-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 ce439d961c5806d62c02572a1790a6b6591aad1a..16e6e9da7ff478b574edcc5f5756da5ac302ed34 100644 (file)
--- a/helm/software/components/hmysql/.depend
+++ b/helm/software/components/hmysql/.depend
@@ -1,7 +1,2 @@
-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 c2289bff28e2b3c806b7240252460a805274a528..602c901b81f28e6d8f557a971cd84673bfb701c9 100644 (file)
--- a/helm/software/components/hmysql/.depend.opt
+++ b/helm/software/components/hmysql/.depend.opt
@@ -1,7 +1,2 @@
-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 16c1145165e3acf1c2c923e16a634ce3f3967bef..847a4a807733e1ff71a24f44d6ff3ed18dd0252b 100644 (file)
--- a/helm/software/components/lexicon/.depend
+++ b/helm/software/components/lexicon/.depend
@@ -3,8 +3,6 @@ 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 0fee4b18e0ea1c8028d8a00805d03f848b06c55d..463d8a7bc2ab55bca12b9ff9c3ecfbb4e7bf222b 100644 (file)
--- a/helm/software/components/lexicon/.depend.opt
+++ b/helm/software/components/lexicon/.depend.opt
@@ -3,8 +3,6 @@ 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 cfa1295edcd418319d423cb3ad3f4cc106a1ff21..a9f24f814f3dfb119e00e1fe2f6d71ef565d38ff 100644 (file)
--- a/helm/software/components/library/.depend
+++ b/helm/software/components/library/.depend
@@ -1,13 +1,4 @@
-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 cfa1295edcd418319d423cb3ad3f4cc106a1ff21..a9f24f814f3dfb119e00e1fe2f6d71ef565d38ff 100644 (file)
--- a/helm/software/components/library/.depend.opt
+++ b/helm/software/components/library/.depend.opt
@@ -1,13 +1,4 @@
-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 dfb4400ff0dce00c92943043edccecc0c1222ed5..28268d29ee15cd05d86a0565b7d47abfe8ecf81f 100644 (file)
--- a/helm/software/components/logger/.depend
+++ b/helm/software/components/logger/.depend
@@ -1,3 +1,2 @@
-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 dfb4400ff0dce00c92943043edccecc0c1222ed5..28268d29ee15cd05d86a0565b7d47abfe8ecf81f 100644 (file)
--- a/helm/software/components/logger/.depend.opt
+++ b/helm/software/components/logger/.depend.opt
@@ -1,3 +1,2 @@
-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 78cd97a0deff8787b73aed2878acef8374029ee0..492a34e3a9dad11aa9a08d4a09802647c6e0bf95 100644 (file)
--- a/helm/software/components/metadata/.depend
+++ b/helm/software/components/metadata/.depend
@@ -1,5 +1,3 @@
-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 78cd97a0deff8787b73aed2878acef8374029ee0..492a34e3a9dad11aa9a08d4a09802647c6e0bf95 100644 (file)
--- a/helm/software/components/metadata/.depend.opt
+++ b/helm/software/components/metadata/.depend.opt
@@ -1,5 +1,3 @@
-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 1316c8eab83e4c08ca7047ed72175492e98197a1..b4e17fa99bca931a5289d06541f5b69060d11594 100644 (file)
--- a/helm/software/components/ng_cic_content/.depend
+++ b/helm/software/components/ng_cic_content/.depend
@@ -1,5 +1,3 @@
-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 1316c8eab83e4c08ca7047ed72175492e98197a1..b4e17fa99bca931a5289d06541f5b69060d11594 100644 (file)
--- a/helm/software/components/ng_cic_content/.depend.opt
+++ b/helm/software/components/ng_cic_content/.depend.opt
@@ -1,5 +1,3 @@
-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 2de54dc5eaedce21d8850cc5f76cc76f38331752..6b4ef95c1ee75472df6140057f1b06851033b996 100644 (file)
--- a/helm/software/components/ng_disambiguation/.depend
+++ b/helm/software/components/ng_disambiguation/.depend
@@ -1,3 +1,2 @@
-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 2de54dc5eaedce21d8850cc5f76cc76f38331752..6b4ef95c1ee75472df6140057f1b06851033b996 100644 (file)
--- a/helm/software/components/ng_disambiguation/.depend.opt
+++ b/helm/software/components/ng_disambiguation/.depend.opt
@@ -1,3 +1,2 @@
-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 aeb011ffc063760795ca97c637156a210e065b14..159cee38249f5ad9aee129b4df6a0c1de6db9f02 100644 (file)
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -1,4 +1,3 @@
-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 332deb32c72fc54f1dd7923d9b4525261d7ecb8a..01056b468c95b1f692351032f64b129584770b53 100644 (file)
--- a/helm/software/components/ng_kernel/.depend.opt
+++ b/helm/software/components/ng_kernel/.depend.opt
@@ -1,4 +1,3 @@
-nUri.cmi: 
 nReference.cmi: nUri.cmi 
 nCicUtils.cmi: nCic.cmx 
 nCicSubstitution.cmi: nCic.cmx 

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index 369ed6b69068acbe0644b42cf2d38e8f5bb48c02..3ace5101400f920267785840a298257e8a1a2078 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -1,4 +1,3 @@
-terms.cmi: 
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
@@ -11,7 +10,6 @@ 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 369ed6b69068acbe0644b42cf2d38e8f5bb48c02..3ace5101400f920267785840a298257e8a1a2078 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend.opt
+++ b/helm/software/components/ng_paramodulation/.depend.opt
@@ -1,4 +1,3 @@
-terms.cmi: 
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
@@ -11,7 +10,6 @@ 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 db7e5288428cc5c63f47f29ba31c99d41f9412d3..f30b906fd908a88f33150931a8bd8e0d5d232e35 100644 (file)
--- a/helm/software/components/ng_refiner/.depend
+++ b/helm/software/components/ng_refiner/.depend
@@ -1,6 +1,3 @@
-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 db7e5288428cc5c63f47f29ba31c99d41f9412d3..f30b906fd908a88f33150931a8bd8e0d5d232e35 100644 (file)
--- a/helm/software/components/ng_refiner/.depend.opt
+++ b/helm/software/components/ng_refiner/.depend.opt
@@ -1,6 +1,3 @@
-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 8d3bcd0c132285492ac8bf9fbfb6baabfcee24b1..86ae2b375fcbbbc274d2917d6254aec5d68b5b58 100644 (file)
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,6 +1,3 @@
-nCicTacReduction.cmi: 
-nTacStatus.cmi: 
-nCicElim.cmi: 
 nTactics.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
@@ -11,5 +8,5 @@ nCicElim.cmo: nCicElim.cmi
 nCicElim.cmx: nCicElim.cmi 
 nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
 nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi 
-nInversion.cmo: nTactics.cmi nInversion.cmi 
-nInversion.cmx: nTactics.cmx nInversion.cmi 
+nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi 
+nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi 

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

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 366697ece6adff18d955b417a488bddef1015a79..a93e7f5131ad6d23bbda4735e16967ab1af4cbf3 100644 (file)
--- a/helm/software/components/ng_tactics/nInversion.ml
+++ b/helm/software/components/ng_tactics/nInversion.ml
@@ -49,10 +49,14 @@ let rec mk_lambdas l t =
   | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t)
 ;;
 
-let rec mk_arrows l t =
-  match l with
-    [] -> t
-  | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id "_", Some hd), mk_arrows tl t)
+let rec mk_arrows xs ys selection target = 
+  match selection,xs,ys with
+    [],[],[] -> target
+  | false :: l,x::xs,y::ys -> mk_arrows xs ys l target
+  | true :: l,x::xs,y::ys  -> 
+     CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
+                           mk_arrows xs ys l target)
+  | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
 ;;
 
 let subst_metasenv_and_fix_names status =
@@ -64,7 +68,7 @@ let subst_metasenv_and_fix_names status =
    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
 ;;
 
-let mk_inverter name it leftno status baseuri =
+let mk_inverter name it leftno ?selection outsort status baseuri =
  prerr_endline ("leftno = " ^ string_of_int leftno);
  let _,ind_name,ty,cl = it in
  prerr_endline ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
@@ -72,13 +76,13 @@ let mk_inverter name it leftno status baseuri =
  (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
  let params = List.rev_map (function name,_ -> mk_id name) params in
  prerr_endline ("lunghezza params = " ^ string_of_int (List.length params));*)
- let args,sort = split_arity ~subst:[] [] ty in
+ let args,sort= split_arity ~subst:[] [] ty in
  prerr_endline ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort);
  (*let args = List.rev_map (function name,_ -> mk_id name) args in
  prerr_endline ("lunghezza args = " ^ string_of_int (List.length args));*)
  let nparams = List.length args in
  prerr_endline ("nparams = " ^ string_of_int nparams);
-
+ 
  let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
  prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs));
  let ls, rs = HExtlib.split_nth leftno xs in
@@ -97,17 +101,11 @@ let mk_inverter name it leftno status baseuri =
  (* pred := P yr- *)
  let pred = mk_appl ((mk_id "P")::id_ys) in
  
- let selection = HExtlib.mk_list true (List.length ys) in
- let prods =
-   let rec prodaux = function
-       [],[],[] -> pred
-     | false :: l,x::xs,y::ys -> prodaux (l,xs,ys)
-     | true :: l,x::xs,y::ys  -> 
-        CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
-                              prodaux (l,xs,ys))
-     | _ -> assert false
-   in prodaux (selection,id_rs,id_ys)
+ let selection = match selection with 
+     None -> HExtlib.mk_list true (List.length ys) 
+   | Some s -> s
  in
+ let prods = mk_arrows id_rs id_ys selection pred in
 
  let lambdas = mk_lambdas (ys@["p"]) prods in
  
@@ -118,21 +116,21 @@ let mk_inverter name it leftno status baseuri =
    in (hypaux 1 ncons)
  in
  prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys));
+
+ let outsort, suffix = NCicElim.ast_of_sort outsort in
  let theorem = mk_prods xs
-                (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort `Prop))),
+                (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))),
                 mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *)
                                   Some (CicNotationPt.Implicit `JustOne)),
                                   mk_appl (mk_id "P"::id_rs)))))
  in 
- let t = mk_appl ( [mk_id (ind_name ^ "_ind"); lambdas] @
+ let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix); lambdas] @
                    List.map mk_id hyplist @
                    CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in
 
- prerr_endline ("NINVERTER 0");
  let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
                          (baseuri ^ name ^ ".def",
                            0,CicNotationPt.Theorem (`Theorem,name,theorem,Some (CicNotationPt.Implicit (`Tagged "inv")))) in 
- prerr_endline ("NINVERTER 1");
  let uri,height,nmenv,nsubst,nobj = theorem in
  let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
  let status = status#set_obj theorem in
@@ -140,21 +138,14 @@ let mk_inverter name it leftno status baseuri =
  let status = subst_metasenv_and_fix_names status in
 
  let cut_theorem = 
-   mk_arrows (List.map 
-     (fun x -> let x = mk_id x in mk_appl [mk_id "eq";
-                                           CicNotationPt.Implicit `JustOne;
-                                           x;x]) rs) (mk_appl (mk_id "P"::List.map mk_id rs)) in
+   let rs = List.map (fun x -> mk_id x) rs in
+     mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in
+
  let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
                     CicNotationPt.Implicit (`Tagged "end"));
                     CicNotationPt.Implicit (`Tagged "cut")] in
  
  let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
- (*let branches = 
-   let rec branch_aux k = function 
-       0 -> [NTactics.apply_tac ("",0,mk_id "H")]
-     | n -> NTactics.apply_tac ("",0,mk_id ("H"^(string_of_int k)))::(branch_aux (k+1) (n-1))
-   in branch_aux 1 ncons
- in*)
  
  let status = NTactics.block_tac 
                         (NTactics.branch_tac::
@@ -163,34 +154,13 @@ let mk_inverter name it leftno status baseuri =
                           [NTactics.apply_tac ("",0,cut);
                            NTactics.branch_tac;
                            NTactics.case_tac "end";
-                           (*NTactics.intro_tac "Hcut";*)
                            NTactics.apply_tac ("",0,mk_id "Hcut");
                            NTactics.apply_tac ("",0,mk_id "refl_eq"); 
                            NTactics.shift_tac;
                            NTactics.case_tac "cut";
                            NTactics.apply_tac ("",0,t);
-                        (*   NTactics.branch_tac]
-                          @ branches @ 
-                          [NTactics.merge_tac; *)
                            NTactics.merge_tac;
                            NTactics.merge_tac;
                            NTactics.skip_tac])) status in
  status,status#obj
 ;;
-
-
-let ast_of_sort s =
-  match s with
-     NCic.Prop -> `Prop,"ind"
-   | NCic.Type u ->
-      let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
-      (try
-        if String.sub u 0 4 = "Type" then
-         `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
-        else if String.sub u 0 5 = "CProp" then
-         `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
-        else
-         (prerr_endline u;
-         assert false)
-       with Failure _ -> assert false)
-;;

diff --git a/helm/software/components/ng_tactics/nInversion.mli b/helm/software/components/ng_tactics/nInversion.mli
index 4d6de91ed5898333be4871098700353dd7cd2944..b5ca8597d9b53f0f13bf0875c22b912c86034c07 100644 (file)
--- a/helm/software/components/ng_tactics/nInversion.mli
+++ b/helm/software/components/ng_tactics/nInversion.mli
@@ -11,5 +11,6 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val mk_inverter: string -> NCic.inductiveType -> int -> (#NTacStatus.tac_status as 's) -> string -> 's * NCic.obj
-
+val mk_inverter: string -> NCic.inductiveType -> int -> ?selection:bool list ->
+  NCic.sort -> (#NTacStatus.tac_status as 's) -> string -> 
+  's * NCic.obj

diff --git a/helm/software/components/registry/.depend b/helm/software/components/registry/.depend
index 40c03891a7433c13e27e38dbe1cb51e06030c905..cf4f36b68f502fc728be91d4b20e8b0dcd3658f2 100644 (file)
--- a/helm/software/components/registry/.depend
+++ b/helm/software/components/registry/.depend
@@ -1,3 +1,2 @@
-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 40c03891a7433c13e27e38dbe1cb51e06030c905..cf4f36b68f502fc728be91d4b20e8b0dcd3658f2 100644 (file)
--- a/helm/software/components/registry/.depend.opt
+++ b/helm/software/components/registry/.depend.opt
@@ -1,3 +1,2 @@
-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 25e67131fca0487c4390d310d8307722b5058067..f3c6a8bd17a7351e99ce8e59905fda76a37cbf08 100644 (file)
--- a/helm/software/components/syntax_extensions/.depend
+++ b/helm/software/components/syntax_extensions/.depend
@@ -1,5 +1,2 @@
-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 3d7dfc21fef76318d2516be6b5736428108d2d02..c0cd9c9069420ca3c124fdf3a0f152838c5d121e 100644 (file)
--- a/helm/software/components/syntax_extensions/.depend.opt
+++ b/helm/software/components/syntax_extensions/.depend.opt
@@ -1,5 +1,2 @@
-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 d9d6034a11e090bef20f2d14ccd1d8fb4e5692e2..169fc76b0e21d9fad98c2fa23430aeb0fa3a0f81 100644 (file)
--- a/helm/software/components/tactics/.depend
+++ b/helm/software/components/tactics/.depend
@@ -1,19 +1,11 @@
-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 
@@ -35,13 +27,10 @@ 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 d9d6034a11e090bef20f2d14ccd1d8fb4e5692e2..169fc76b0e21d9fad98c2fa23430aeb0fa3a0f81 100644 (file)
--- a/helm/software/components/tactics/.depend.opt
+++ b/helm/software/components/tactics/.depend.opt
@@ -1,19 +1,11 @@
-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 
@@ -35,13 +27,10 @@ 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 6616a03d0f4c0803fa1e9c2e309bbf89270e7526..7759190c66cdd57bcc79c0da85a571cd76faa730 100644 (file)
--- a/helm/software/components/thread/.depend
+++ b/helm/software/components/thread/.depend
@@ -1,5 +1,3 @@
-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 6616a03d0f4c0803fa1e9c2e309bbf89270e7526..7759190c66cdd57bcc79c0da85a571cd76faa730 100644 (file)
--- a/helm/software/components/thread/.depend.opt
+++ b/helm/software/components/thread/.depend.opt
@@ -1,5 +1,3 @@
-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 a8972f4cfc20c049020440e4f567cfb622de8243..bc310327f83551dd5875e62bfa3899e7c55559a2 100644 (file)
--- a/helm/software/components/tptp_grafite/.depend
+++ b/helm/software/components/tptp_grafite/.depend
@@ -1,7 +1,4 @@
 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 fb60fe8f2d6ae59e0b1b46ae5675794888fd335f..c74300207fb532cff81cbdcd6146f285a05a7599 100644 (file)
--- a/helm/software/components/tptp_grafite/.depend.opt
+++ b/helm/software/components/tptp_grafite/.depend.opt
@@ -1,7 +1,4 @@
 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 9cac9aa783c7c003e70e118017c77b20d2ccb61a..4821484239ac15df403da8d9123671544b3aa65f 100644 (file)
--- a/helm/software/components/urimanager/.depend
+++ b/helm/software/components/urimanager/.depend
@@ -1,3 +1,2 @@
-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 9cac9aa783c7c003e70e118017c77b20d2ccb61a..4821484239ac15df403da8d9123671544b3aa65f 100644 (file)
--- a/helm/software/components/urimanager/.depend.opt
+++ b/helm/software/components/urimanager/.depend.opt
@@ -1,3 +1,2 @@
-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 65dc079553f6476748ecdb106d61534fa746d753..39f37dfa90077f1212c1f51f57ef8c55a21174c7 100644 (file)
--- a/helm/software/components/whelp/.depend
+++ b/helm/software/components/whelp/.depend
@@ -1,5 +1,3 @@
-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 65dc079553f6476748ecdb106d61534fa746d753..39f37dfa90077f1212c1f51f57ef8c55a21174c7 100644 (file)
--- a/helm/software/components/whelp/.depend.opt
+++ b/helm/software/components/whelp/.depend.opt
@@ -1,5 +1,3 @@
-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 e7e7ffbd729fcdbc6206eb38afebf53940878718..5ef59bdc96d40e0a64e0f50d91b949382a7f57e0 100644 (file)
--- a/helm/software/components/xml/.depend
+++ b/helm/software/components/xml/.depend
@@ -1,5 +1,3 @@
-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 e7e7ffbd729fcdbc6206eb38afebf53940878718..5ef59bdc96d40e0a64e0f50d91b949382a7f57e0 100644 (file)
--- a/helm/software/components/xml/.depend.opt
+++ b/helm/software/components/xml/.depend.opt
@@ -1,5 +1,3 @@
-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 65bd7b9496155f928775a264636cae0249c62a98..e2832de332dd83fb5bd4beb1cd2b1e735d6fe35e 100644 (file)
--- a/helm/software/components/xmldiff/.depend
+++ b/helm/software/components/xmldiff/.depend
@@ -1,3 +1,2 @@
-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 65bd7b9496155f928775a264636cae0249c62a98..e2832de332dd83fb5bd4beb1cd2b1e735d6fe35e 100644 (file)
--- a/helm/software/components/xmldiff/.depend.opt
+++ b/helm/software/components/xmldiff/.depend.opt
@@ -1,3 +1,2 @@
-xmlDiff.cmi: 
 xmlDiff.cmo: xmlDiff.cmi 
 xmlDiff.cmx: xmlDiff.cmi