- now destruct tries to clear the replaced variables (from wilmer's

patch)
- dependences update

diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt
index aec750131fea643a21c2d3c9e8505d303845adf0..34a327264c78f0574a21439a20b51f42b849ff21 100644 (file)
--- a/matita/components/content/.depend.opt
+++ b/matita/components/content/.depend.opt
@@ -1,14 +1,14 @@
-content.cmi:
-notationUtil.cmi: notationPt.cmx
-notationEnv.cmi: notationPt.cmx
-notationPp.cmi: notationPt.cmx notationEnv.cmi
-notationPt.cmo:
-notationPt.cmx:
-content.cmo: content.cmi
-content.cmx: content.cmi
-notationUtil.cmo: notationPt.cmx notationUtil.cmi
-notationUtil.cmx: notationPt.cmx notationUtil.cmi
-notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi
-notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi
-notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi
+content.cmi: 
+notationUtil.cmi: notationPt.cmx 
+notationEnv.cmi: notationPt.cmx 
+notationPp.cmi: notationPt.cmx notationEnv.cmi 
+notationPt.cmo: 
+notationPt.cmx: 
+content.cmo: content.cmi 
+content.cmx: content.cmi 
+notationUtil.cmo: notationPt.cmx notationUtil.cmi 
+notationUtil.cmx: notationPt.cmx notationUtil.cmi 
+notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi 
+notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi 
+notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi 
+notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi 

diff --git a/matita/components/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt
index 03a1732eb9be3f3c8e2d1aeaebc618438c4433a0..5c11c1ded8262405d4b965fa534115da4d9f00c3 100644 (file)
--- a/matita/components/content_pres/.depend.opt
+++ b/matita/components/content_pres/.depend.opt
@@ -1,38 +1,38 @@
-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
-content2pres.cmi: termContentPres.cmi cicNotationPres.cmi
-renderingAttrs.cmo: renderingAttrs.cmi
-renderingAttrs.cmx: renderingAttrs.cmi
-cicNotationLexer.cmo: cicNotationLexer.cmi
-cicNotationLexer.cmx: cicNotationLexer.cmi
-cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi
-cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi
-mpresentation.cmo: mpresentation.cmi
-mpresentation.cmx: mpresentation.cmi
-box.cmo: renderingAttrs.cmi box.cmi
-box.cmx: renderingAttrs.cmx box.cmi
-content2presMatcher.cmo: content2presMatcher.cmi
-content2presMatcher.cmx: content2presMatcher.cmi
+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 
+content2pres.cmi: termContentPres.cmi cicNotationPres.cmi 
+renderingAttrs.cmo: renderingAttrs.cmi 
+renderingAttrs.cmx: renderingAttrs.cmi 
+cicNotationLexer.cmo: cicNotationLexer.cmi 
+cicNotationLexer.cmx: cicNotationLexer.cmi 
+cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi 
+cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi 
+mpresentation.cmo: mpresentation.cmi 
+mpresentation.cmx: mpresentation.cmi 
+box.cmo: renderingAttrs.cmi box.cmi 
+box.cmx: renderingAttrs.cmx box.cmi 
+content2presMatcher.cmo: content2presMatcher.cmi 
+content2presMatcher.cmx: content2presMatcher.cmi 
 termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \
-    cicNotationParser.cmi termContentPres.cmi
+    cicNotationParser.cmi termContentPres.cmi 
 termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \
-    cicNotationParser.cmx termContentPres.cmi
+    cicNotationParser.cmx termContentPres.cmi 
 boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
-    boxPp.cmi
+    boxPp.cmi 
 boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
-    boxPp.cmi
+    boxPp.cmi 
 cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
-    cicNotationPres.cmi
+    cicNotationPres.cmi 
 cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
-    cicNotationPres.cmi
+    cicNotationPres.cmi 
 content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
-    cicNotationPres.cmi box.cmi content2pres.cmi
+    cicNotationPres.cmi box.cmi content2pres.cmi 
 content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
-    cicNotationPres.cmx box.cmx content2pres.cmi
+    cicNotationPres.cmx box.cmx content2pres.cmi 

diff --git a/matita/components/disambiguation/.depend.opt b/matita/components/disambiguation/.depend.opt
index fa6388aa7985f952fcfc356d09d10e7b467b7812..9fdbeeeafa878cfe32dbf1f96adaad1e3044a4eb 100644 (file)
--- a/matita/components/disambiguation/.depend.opt
+++ b/matita/components/disambiguation/.depend.opt
@@ -1,11 +1,11 @@
-disambiguateTypes.cmi:
-disambiguate.cmi: disambiguateTypes.cmi
-multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
-disambiguateTypes.cmo: disambiguateTypes.cmi
-disambiguateTypes.cmx: disambiguateTypes.cmi
-disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi
-disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi
+disambiguateTypes.cmi: 
+disambiguate.cmi: disambiguateTypes.cmi 
+multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi 
+disambiguateTypes.cmo: disambiguateTypes.cmi 
+disambiguateTypes.cmx: disambiguateTypes.cmi 
+disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi 
+disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi 
 multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \
-    multiPassDisambiguator.cmi
+    multiPassDisambiguator.cmi 
 multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \
-    multiPassDisambiguator.cmi
+    multiPassDisambiguator.cmi 

diff --git a/matita/components/extlib/.depend.opt b/matita/components/extlib/.depend.opt
index b121fbcd1d810f4f0921c4580bf8700bf63fc66a..6f707effcd8f40c3cca0262be1d045e17b98c5d2 100644 (file)
--- a/matita/components/extlib/.depend.opt
+++ b/matita/components/extlib/.depend.opt
@@ -1,27 +1,27 @@
-componentsConf.cmi:
-hExtlib.cmi:
-hMarshal.cmi:
-patternMatcher.cmi:
-hLog.cmi:
-trie.cmi:
-discrimination_tree.cmi:
-hTopoSort.cmi:
-graphvizPp.cmi:
-componentsConf.cmo: componentsConf.cmi
-componentsConf.cmx: componentsConf.cmi
-hExtlib.cmo: hExtlib.cmi
-hExtlib.cmx: hExtlib.cmi
-hMarshal.cmo: hExtlib.cmi hMarshal.cmi
-hMarshal.cmx: hExtlib.cmx hMarshal.cmi
-patternMatcher.cmo: patternMatcher.cmi
-patternMatcher.cmx: patternMatcher.cmi
-hLog.cmo: hLog.cmi
-hLog.cmx: hLog.cmi
-trie.cmo: trie.cmi
-trie.cmx: trie.cmi
-discrimination_tree.cmo: trie.cmi hExtlib.cmi discrimination_tree.cmi
-discrimination_tree.cmx: trie.cmx hExtlib.cmx discrimination_tree.cmi
-hTopoSort.cmo: hTopoSort.cmi
-hTopoSort.cmx: hTopoSort.cmi
-graphvizPp.cmo: graphvizPp.cmi
-graphvizPp.cmx: graphvizPp.cmi
+componentsConf.cmi: 
+hExtlib.cmi: 
+hMarshal.cmi: 
+patternMatcher.cmi: 
+hLog.cmi: 
+trie.cmi: 
+discrimination_tree.cmi: 
+hTopoSort.cmi: 
+graphvizPp.cmi: 
+componentsConf.cmo: componentsConf.cmi 
+componentsConf.cmx: componentsConf.cmi 
+hExtlib.cmo: hExtlib.cmi 
+hExtlib.cmx: hExtlib.cmi 
+hMarshal.cmo: hExtlib.cmi hMarshal.cmi 
+hMarshal.cmx: hExtlib.cmx hMarshal.cmi 
+patternMatcher.cmo: patternMatcher.cmi 
+patternMatcher.cmx: patternMatcher.cmi 
+hLog.cmo: hLog.cmi 
+hLog.cmx: hLog.cmi 
+trie.cmo: trie.cmi 
+trie.cmx: trie.cmi 
+discrimination_tree.cmo: trie.cmi hExtlib.cmi discrimination_tree.cmi 
+discrimination_tree.cmx: trie.cmx hExtlib.cmx discrimination_tree.cmi 
+hTopoSort.cmo: hTopoSort.cmi 
+hTopoSort.cmx: hTopoSort.cmi 
+graphvizPp.cmo: graphvizPp.cmi 
+graphvizPp.cmx: graphvizPp.cmi 

diff --git a/matita/components/getter/.depend.opt b/matita/components/getter/.depend.opt
index 301b9d8b8913b8ac1a59fabe9228c465908e12ba..64da37f137deef8a5baebcbd07ba8f62cbf8e39c 100644 (file)
--- a/matita/components/getter/.depend.opt
+++ b/matita/components/getter/.depend.opt
@@ -1,38 +1,38 @@
-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
-http_getter_logger.cmx: http_getter_logger.cmi
-http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi
-http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi
-http_getter_const.cmo: http_getter_const.cmi
-http_getter_const.cmx: http_getter_const.cmi
+http_getter_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 
+http_getter_logger.cmx: http_getter_logger.cmi 
+http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi 
+http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi 
+http_getter_const.cmo: http_getter_const.cmi 
+http_getter_const.cmx: http_getter_const.cmi 
 http_getter_env.cmo: http_getter_types.cmx http_getter_misc.cmi \
-    http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi
+    http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi 
 http_getter_env.cmx: http_getter_types.cmx http_getter_misc.cmx \
-    http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
+    http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi 
 http_getter_storage.cmo: http_getter_wget.cmi http_getter_types.cmx \
-    http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi
+    http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi 
 http_getter_storage.cmx: http_getter_wget.cmx http_getter_types.cmx \
-    http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
+    http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi 
 http_getter_common.cmo: http_getter_types.cmx http_getter_misc.cmi \
-    http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi
+    http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi 
 http_getter_common.cmx: http_getter_types.cmx http_getter_misc.cmx \
-    http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
+    http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi 
 http_getter.cmo: http_getter_wget.cmi http_getter_types.cmx \
     http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \
     http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \
-    http_getter.cmi
+    http_getter.cmi 
 http_getter.cmx: http_getter_wget.cmx http_getter_types.cmx \
     http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
     http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
-    http_getter.cmi
+    http_getter.cmi 

diff --git a/matita/components/grafite/.depend.opt b/matita/components/grafite/.depend.opt
index fbe333cbde84ceaa7c79f57cefa7941100528d12..3a2590d84f29a7b2f661891c3dc88eb48acb9589 100644 (file)
--- a/matita/components/grafite/.depend.opt
+++ b/matita/components/grafite/.depend.opt
@@ -1,5 +1,5 @@
-grafiteAstPp.cmi: grafiteAst.cmx
-grafiteAst.cmo:
-grafiteAst.cmx:
-grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi
-grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
+grafiteAstPp.cmi: grafiteAst.cmx 
+grafiteAst.cmo: 
+grafiteAst.cmx: 
+grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi 
+grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi 

diff --git a/matita/components/grafite_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt
index 27787b008a0fd68ab2fe0e21a32de1e5bc0d977e..d04ec9d2cde36b3190498a3b7d0820a0a859878a 100644 (file)
--- a/matita/components/grafite_engine/.depend.opt
+++ b/matita/components/grafite_engine/.depend.opt
@@ -1,11 +1,11 @@
-grafiteTypes.cmi:
-nCicCoercDeclaration.cmi: grafiteTypes.cmi
-grafiteEngine.cmi: grafiteTypes.cmi
-grafiteTypes.cmo: grafiteTypes.cmi
-grafiteTypes.cmx: grafiteTypes.cmi
-nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi
-nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi
+grafiteTypes.cmi: 
+nCicCoercDeclaration.cmi: grafiteTypes.cmi 
+grafiteEngine.cmi: grafiteTypes.cmi 
+grafiteTypes.cmo: grafiteTypes.cmi 
+grafiteTypes.cmx: grafiteTypes.cmi 
+nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi 
+nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi 
 grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \
-    grafiteEngine.cmi
+    grafiteEngine.cmi 
 grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \
-    grafiteEngine.cmi
+    grafiteEngine.cmi 

diff --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt
index 5142da1bf4ce3d4744fd0df8c6ea3070f545436c..e5cd5f2b357785b3a6ea40ea0ec42b06723ecd31 100644 (file)
--- a/matita/components/grafite_parser/.depend.opt
+++ b/matita/components/grafite_parser/.depend.opt
@@ -1,6 +1,6 @@
-grafiteParser.cmi:
-print_grammar.cmi: grafiteParser.cmi
-grafiteParser.cmo: grafiteParser.cmi
-grafiteParser.cmx: grafiteParser.cmi
-print_grammar.cmo: print_grammar.cmi
-print_grammar.cmx: print_grammar.cmi
+grafiteParser.cmi: 
+print_grammar.cmi: grafiteParser.cmi 
+grafiteParser.cmo: grafiteParser.cmi 
+grafiteParser.cmx: grafiteParser.cmi 
+print_grammar.cmo: print_grammar.cmi 
+print_grammar.cmx: print_grammar.cmi 

diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt
index 28703386aad00a4e2a16e2783eefcc8461815e3e..edb2abe955afe4357fc9126c8296ddf87dd7247c 100644 (file)
--- a/matita/components/library/.depend.opt
+++ b/matita/components/library/.depend.opt
@@ -1,9 +1,9 @@
-librarian.cmi:
-libraryMisc.cmi:
-libraryClean.cmi:
-librarian.cmo: librarian.cmi
-librarian.cmx: librarian.cmi
-libraryMisc.cmo: libraryMisc.cmi
-libraryMisc.cmx: libraryMisc.cmi
-libraryClean.cmo: libraryClean.cmi
-libraryClean.cmx: libraryClean.cmi
+librarian.cmi: 
+libraryMisc.cmi: 
+libraryClean.cmi: 
+librarian.cmo: librarian.cmi 
+librarian.cmx: librarian.cmi 
+libraryMisc.cmo: libraryMisc.cmi 
+libraryMisc.cmx: libraryMisc.cmi 
+libraryClean.cmo: libraryClean.cmi 
+libraryClean.cmx: libraryClean.cmi 

diff --git a/matita/components/logger/.depend.opt b/matita/components/logger/.depend.opt
index 1c8ec5b7c84887d66524df89f46cd7730c64fcc4..dfb4400ff0dce00c92943043edccecc0c1222ed5 100644 (file)
--- a/matita/components/logger/.depend.opt
+++ b/matita/components/logger/.depend.opt
@@ -1,3 +1,3 @@
-helmLogger.cmi:
-helmLogger.cmo: helmLogger.cmi
-helmLogger.cmx: helmLogger.cmi
+helmLogger.cmi: 
+helmLogger.cmo: helmLogger.cmi 
+helmLogger.cmx: helmLogger.cmi 

diff --git a/matita/components/ng_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt
index b1a499fd3facc2d07103b73c013e3750d0b151da..fd1b831b97eb9e4179c3715167b63b20f2b31807 100644 (file)
--- a/matita/components/ng_cic_content/.depend.opt
+++ b/matita/components/ng_cic_content/.depend.opt
@@ -1,6 +1,6 @@
-ncic2astMatcher.cmi:
-interpretations.cmi:
-ncic2astMatcher.cmo: ncic2astMatcher.cmi
-ncic2astMatcher.cmx: ncic2astMatcher.cmi
-interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi
-interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi
+ncic2astMatcher.cmi: 
+interpretations.cmi: 
+ncic2astMatcher.cmo: ncic2astMatcher.cmi 
+ncic2astMatcher.cmx: ncic2astMatcher.cmi 
+interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi 
+interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi 

diff --git a/matita/components/ng_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt
index d5306074ab892a33a75040bd24e990df97bc7357..0810bc8be9c2e8dce0593616b49c54eb617d961b 100644 (file)
--- a/matita/components/ng_disambiguation/.depend.opt
+++ b/matita/components/ng_disambiguation/.depend.opt
@@ -1,14 +1,14 @@
-nnumber_notation.cmi:
-disambiguateChoices.cmi:
-nCicDisambiguate.cmi:
-grafiteDisambiguate.cmi:
-nnumber_notation.cmo: nnumber_notation.cmi
-nnumber_notation.cmx: nnumber_notation.cmi
-disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi
-disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi
-nCicDisambiguate.cmo: nCicDisambiguate.cmi
-nCicDisambiguate.cmx: nCicDisambiguate.cmi
+nnumber_notation.cmi: 
+disambiguateChoices.cmi: 
+nCicDisambiguate.cmi: 
+grafiteDisambiguate.cmi: 
+nnumber_notation.cmo: nnumber_notation.cmi 
+nnumber_notation.cmx: nnumber_notation.cmi 
+disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi 
+disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi 
+nCicDisambiguate.cmo: nCicDisambiguate.cmi 
+nCicDisambiguate.cmx: nCicDisambiguate.cmi 
 grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \
-    grafiteDisambiguate.cmi
+    grafiteDisambiguate.cmi 
 grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \
-    grafiteDisambiguate.cmi
+    grafiteDisambiguate.cmi 

diff --git a/matita/components/ng_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt
index c57bf8efed34aac283e8464783f90cac2e1ed6c6..5e4dabb6ac920a9e9414d4af9cd76d05bf9a2b7a 100644 (file)
--- a/matita/components/ng_kernel/.depend.opt
+++ b/matita/components/ng_kernel/.depend.opt
@@ -1,41 +1,41 @@
-nUri.cmi:
-nReference.cmi: nUri.cmi
-nCicUtils.cmi: nCic.cmx
-nCicSubstitution.cmi: nCic.cmx
-nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx
-nCicReduction.cmi: nCic.cmx
-nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx
-nCicUntrusted.cmi: nCic.cmx
-nCicPp.cmi: nReference.cmi nCic.cmx
-nCic.cmo: nUri.cmi nReference.cmi
-nCic.cmx: nUri.cmx nReference.cmx
-nUri.cmo: nUri.cmi
-nUri.cmx: nUri.cmi
-nReference.cmo: nUri.cmi nReference.cmi
-nReference.cmx: nUri.cmx nReference.cmi
-nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi
-nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi
+nUri.cmi: 
+nReference.cmi: nUri.cmi 
+nCicUtils.cmi: nCic.cmx 
+nCicSubstitution.cmi: nCic.cmx 
+nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx 
+nCicReduction.cmi: nCic.cmx 
+nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx 
+nCicUntrusted.cmi: nCic.cmx 
+nCicPp.cmi: nReference.cmi nCic.cmx 
+nCic.cmo: nUri.cmi nReference.cmi 
+nCic.cmx: nUri.cmx nReference.cmx 
+nUri.cmo: nUri.cmi 
+nUri.cmx: nUri.cmi 
+nReference.cmo: nUri.cmi nReference.cmi 
+nReference.cmx: nUri.cmx nReference.cmi 
+nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi 
+nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi 
 nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmx \
-    nCicSubstitution.cmi
+    nCicSubstitution.cmi 
 nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \
-    nCicSubstitution.cmi
-nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi
-nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
+    nCicSubstitution.cmi 
+nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi 
+nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi 
 nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
-    nCicEnvironment.cmi nCic.cmx nCicReduction.cmi
+    nCicEnvironment.cmi nCic.cmx nCicReduction.cmi 
 nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
-    nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
+    nCicEnvironment.cmx nCic.cmx nCicReduction.cmi 
 nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
     nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \
-    nCicTypeChecker.cmi
+    nCicTypeChecker.cmi 
 nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
     nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
-    nCicTypeChecker.cmi
+    nCicTypeChecker.cmi 
 nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
-    nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi
+    nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi 
 nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
-    nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi
+    nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi 
 nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
-    nCicEnvironment.cmi nCic.cmx nCicPp.cmi
+    nCicEnvironment.cmi nCic.cmx nCicPp.cmi 
 nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
-    nCicEnvironment.cmx nCic.cmx nCicPp.cmi
+    nCicEnvironment.cmx nCic.cmx nCicPp.cmi 

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

diff --git a/matita/components/ng_paramodulation/.depend.opt b/matita/components/ng_paramodulation/.depend.opt
index f6eae06d6b5d6c68a181dfeb4545812e1d953e11..2e31be0ec8ab1a01fa448aafc8974673cc406fba 100644 (file)
--- a/matita/components/ng_paramodulation/.depend.opt
+++ b/matita/components/ng_paramodulation/.depend.opt
@@ -1,45 +1,45 @@
-terms.cmi:
-pp.cmi: terms.cmi
-foSubst.cmi: terms.cmi
-orderings.cmi: terms.cmi
-foUtils.cmi: terms.cmi orderings.cmi
-foUnif.cmi: terms.cmi orderings.cmi
-index.cmi: terms.cmi orderings.cmi
-superposition.cmi: terms.cmi orderings.cmi index.cmi
-stats.cmi: terms.cmi orderings.cmi
-paramod.cmi: terms.cmi orderings.cmi
-nCicBlob.cmi: terms.cmi
-nCicProof.cmi: terms.cmi
-nCicParamod.cmi:
-terms.cmo: terms.cmi
-terms.cmx: terms.cmi
-pp.cmo: terms.cmi pp.cmi
-pp.cmx: terms.cmx pp.cmi
-foSubst.cmo: terms.cmi foSubst.cmi
-foSubst.cmx: terms.cmx foSubst.cmi
-orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi
-orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
-foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
-index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi
-index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi
+terms.cmi: 
+pp.cmi: terms.cmi 
+foSubst.cmi: terms.cmi 
+orderings.cmi: terms.cmi 
+foUtils.cmi: terms.cmi orderings.cmi 
+foUnif.cmi: terms.cmi orderings.cmi 
+index.cmi: terms.cmi orderings.cmi 
+superposition.cmi: terms.cmi orderings.cmi index.cmi 
+stats.cmi: terms.cmi orderings.cmi 
+paramod.cmi: terms.cmi orderings.cmi 
+nCicBlob.cmi: terms.cmi 
+nCicProof.cmi: terms.cmi 
+nCicParamod.cmi: 
+terms.cmo: terms.cmi 
+terms.cmx: terms.cmi 
+pp.cmo: terms.cmi pp.cmi 
+pp.cmx: terms.cmx pp.cmi 
+foSubst.cmo: terms.cmi foSubst.cmi 
+foSubst.cmx: terms.cmx foSubst.cmi 
+orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi 
+orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi 
+foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
+foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
+foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
+foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
+index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi 
+index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi 
 superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
-    foUnif.cmi foSubst.cmi superposition.cmi
+    foUnif.cmi foSubst.cmi superposition.cmi 
 superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
-    foUnif.cmx foSubst.cmx superposition.cmi
-stats.cmo: terms.cmi stats.cmi
-stats.cmx: terms.cmx stats.cmi
+    foUnif.cmx foSubst.cmx superposition.cmi 
+stats.cmo: terms.cmi stats.cmi 
+stats.cmx: terms.cmx stats.cmi 
 paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
-    foUtils.cmi foUnif.cmi paramod.cmi
+    foUtils.cmi foUnif.cmi paramod.cmi 
 paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
-    foUtils.cmx foUnif.cmx paramod.cmi
-nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi
-nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi
-nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi
-nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
+    foUtils.cmx foUnif.cmx paramod.cmi 
+nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi 
+nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi 
+nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi 
+nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi 
 nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
-    nCicBlob.cmi nCicParamod.cmi
+    nCicBlob.cmi nCicParamod.cmi 
 nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
-    nCicBlob.cmx nCicParamod.cmi
+    nCicBlob.cmx nCicParamod.cmi 

diff --git a/matita/components/ng_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt
index 5e055ecdc7551278526253a111a618f70f91f278..2633e1abac21ac6b4ebf6134f07b1c495d67565a 100644 (file)
--- a/matita/components/ng_refiner/.depend.opt
+++ b/matita/components/ng_refiner/.depend.opt
@@ -1,25 +1,25 @@
-nDiscriminationTree.cmi:
-nCicMetaSubst.cmi:
-nCicUnifHint.cmi:
-nCicCoercion.cmi: nCicUnifHint.cmi
-nCicRefineUtil.cmi:
-nCicUnification.cmi: nCicCoercion.cmi
-nCicRefiner.cmi: nCicCoercion.cmi
-nDiscriminationTree.cmo: nDiscriminationTree.cmi
-nDiscriminationTree.cmx: nDiscriminationTree.cmi
-nCicMetaSubst.cmo: nCicMetaSubst.cmi
-nCicMetaSubst.cmx: nCicMetaSubst.cmi
-nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi
-nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi
+nDiscriminationTree.cmi: 
+nCicMetaSubst.cmi: 
+nCicUnifHint.cmi: 
+nCicCoercion.cmi: nCicUnifHint.cmi 
+nCicRefineUtil.cmi: 
+nCicUnification.cmi: nCicCoercion.cmi 
+nCicRefiner.cmi: nCicCoercion.cmi 
+nDiscriminationTree.cmo: nDiscriminationTree.cmi 
+nDiscriminationTree.cmx: nDiscriminationTree.cmi 
+nCicMetaSubst.cmo: nCicMetaSubst.cmi 
+nCicMetaSubst.cmx: nCicMetaSubst.cmi 
+nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi 
+nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi 
 nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
-    nCicCoercion.cmi
+    nCicCoercion.cmi 
 nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
-    nCicCoercion.cmi
-nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi
-nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
-nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
+    nCicCoercion.cmi 
+nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi 
+nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi 
+nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi 
+nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi 
 nCicRefiner.cmo: nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
-    nCicCoercion.cmi nCicRefiner.cmi
+    nCicCoercion.cmi nCicRefiner.cmi 
 nCicRefiner.cmx: nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
-    nCicCoercion.cmx nCicRefiner.cmi
+    nCicCoercion.cmx nCicRefiner.cmi 

diff --git a/matita/components/ng_tactics/.depend b/matita/components/ng_tactics/.depend
index 47f203f0afd7f5a2c292d79533eea5517b286812..c85683251c43d6e392df833a778a031f702c4d28 100644 (file)
--- a/matita/components/ng_tactics/.depend
+++ b/matita/components/ng_tactics/.depend
@@ -24,5 +24,7 @@ nDestructTac.cmo: nTactics.cmi nTacStatus.cmi continuationals.cmi \
     nDestructTac.cmi 
 nDestructTac.cmx: nTactics.cmx nTacStatus.cmx continuationals.cmx \
     nDestructTac.cmi 
-nInversion.cmo: nTactics.cmi nCicElim.cmi continuationals.cmi nInversion.cmi 
-nInversion.cmx: nTactics.cmx nCicElim.cmx continuationals.cmx nInversion.cmi 
+nInversion.cmo: nTactics.cmi nTacStatus.cmi nCicElim.cmi continuationals.cmi \
+    nInversion.cmi 
+nInversion.cmx: nTactics.cmx nTacStatus.cmx nCicElim.cmx continuationals.cmx \
+    nInversion.cmi 

diff --git a/matita/components/ng_tactics/.depend.opt b/matita/components/ng_tactics/.depend.opt
index 3e01ca0fba9904f473324a20e3c1db89ce99fc63..c85683251c43d6e392df833a778a031f702c4d28 100644 (file)
--- a/matita/components/ng_tactics/.depend.opt
+++ b/matita/components/ng_tactics/.depend.opt
@@ -1,30 +1,30 @@
-continuationals.cmi:
-nCicTacReduction.cmi:
-nTacStatus.cmi: continuationals.cmi
-nCicElim.cmi:
-nTactics.cmi: nTacStatus.cmi
-nnAuto.cmi: nTacStatus.cmi
-nDestructTac.cmi: nTacStatus.cmi
-nInversion.cmi: nTacStatus.cmi
-continuationals.cmo: continuationals.cmi
-continuationals.cmx: continuationals.cmi
-nCicTacReduction.cmo: nCicTacReduction.cmi
-nCicTacReduction.cmx: nCicTacReduction.cmi
-nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
-nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
-nCicElim.cmo: nCicElim.cmi
-nCicElim.cmx: nCicElim.cmi
-nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
-nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
+continuationals.cmi: 
+nCicTacReduction.cmi: 
+nTacStatus.cmi: continuationals.cmi 
+nCicElim.cmi: 
+nTactics.cmi: nTacStatus.cmi 
+nnAuto.cmi: nTacStatus.cmi 
+nDestructTac.cmi: nTacStatus.cmi 
+nInversion.cmi: nTacStatus.cmi 
+continuationals.cmo: continuationals.cmi 
+continuationals.cmx: continuationals.cmi 
+nCicTacReduction.cmo: nCicTacReduction.cmi 
+nCicTacReduction.cmx: nCicTacReduction.cmi 
+nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi 
+nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi 
+nCicElim.cmo: nCicElim.cmi 
+nCicElim.cmx: nCicElim.cmi 
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi 
+nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi 
 nnAuto.cmo: nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
-    continuationals.cmi nnAuto.cmi
+    continuationals.cmi nnAuto.cmi 
 nnAuto.cmx: nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
-    continuationals.cmx nnAuto.cmi
+    continuationals.cmx nnAuto.cmi 
 nDestructTac.cmo: nTactics.cmi nTacStatus.cmi continuationals.cmi \
-    nDestructTac.cmi
+    nDestructTac.cmi 
 nDestructTac.cmx: nTactics.cmx nTacStatus.cmx continuationals.cmx \
-    nDestructTac.cmi
+    nDestructTac.cmi 
 nInversion.cmo: nTactics.cmi nTacStatus.cmi nCicElim.cmi continuationals.cmi \
-    nInversion.cmi
+    nInversion.cmi 
 nInversion.cmx: nTactics.cmx nTacStatus.cmx nCicElim.cmx continuationals.cmx \
-    nInversion.cmi
+    nInversion.cmi 

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index 12a1efd7ed32cc8a6ba2fd37c78a02de3a1a5ec7..c9e46dc2af1b8523109f4b594705afb33c7435f7 100644 (file)
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -469,6 +469,11 @@ let subst_tac ~context ~dir skip cur_eq =
       | NCic.Rel var ->
         cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq)
       | _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
+    let varname = match var with
+      | NCic.Rel var -> 
+          let name,_ = List.nth context var in [name]
+      | _ -> []
+    in      
     let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
     if (List.exists (fun x -> List.mem x skip) names_to_gen)
       then oldstatus
@@ -487,7 +492,12 @@ let subst_tac ~context ~dir skip cur_eq =
                    ~what:("",0,mk_id eq_name) ~where:default_pattern;
 (*                 NTactics.reduce_tac ~reduction:(`Normalize true)
                    ~where:default_pattern;*)
+                 (* XXX: temo che la clear multipla funzioni bene soltanto se
+                  * gli identificatori sono nell'ordine giusto.
+                  * Per non saper né leggere né scrivere, usiamo due clear
+                  * invece di una *)              
                  NTactics.try_tac (NTactics.clear_tac [eq_name]);
+                NTactics.try_tac (NTactics.clear_tac varname);
 ]@
                  (List.map NTactics.intro_tac (List.rev names_to_gen))) status
 ;;

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

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

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

diff --git a/matita/components/thread/.depend.opt b/matita/components/thread/.depend.opt
index e25145b8b1499b6c59f701cc8a2e4269b3b0e56b..6616a03d0f4c0803fa1e9c2e309bbf89270e7526 100644 (file)
--- a/matita/components/thread/.depend.opt
+++ b/matita/components/thread/.depend.opt
@@ -1,6 +1,6 @@
-threadSafe.cmi:
-extThread.cmi:
-threadSafe.cmo: threadSafe.cmi
-threadSafe.cmx: threadSafe.cmi
-extThread.cmo: extThread.cmi
-extThread.cmx: extThread.cmi
+threadSafe.cmi: 
+extThread.cmi: 
+threadSafe.cmo: threadSafe.cmi 
+threadSafe.cmx: threadSafe.cmi 
+extThread.cmo: extThread.cmi 
+extThread.cmx: extThread.cmi 

diff --git a/matita/components/xml/.depend.opt b/matita/components/xml/.depend.opt
index eda62779ff37dd14feca9e54c864e5ebbd2b7b70..e7e7ffbd729fcdbc6206eb38afebf53940878718 100644 (file)
--- a/matita/components/xml/.depend.opt
+++ b/matita/components/xml/.depend.opt
@@ -1,6 +1,6 @@
-xml.cmi:
-xmlPushParser.cmi:
-xml.cmo: xml.cmi
-xml.cmx: xml.cmi
-xmlPushParser.cmo: xmlPushParser.cmi
-xmlPushParser.cmx: xmlPushParser.cmi
+xml.cmi: 
+xmlPushParser.cmi: 
+xml.cmo: xml.cmi 
+xml.cmx: xml.cmi 
+xmlPushParser.cmo: xmlPushParser.cmi 
+xmlPushParser.cmx: xmlPushParser.cmi 

diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt
index fb48e954caecd96be26ac495ca3bbf19aae8a632..74d8be432f00ee9103d7af42387aaffa5a926228 100644 (file)
--- a/matita/matita/.depend.opt
+++ b/matita/matita/.depend.opt
@@ -1,76 +1,76 @@
-applyTransformation.cmo: applyTransformation.cmi
-applyTransformation.cmx: applyTransformation.cmi
-buildTimeConf.cmo:
-buildTimeConf.cmx:
+applyTransformation.cmo: applyTransformation.cmi 
+applyTransformation.cmx: applyTransformation.cmi 
+buildTimeConf.cmo: 
+buildTimeConf.cmx: 
 cicMathView.cmo: matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
-    buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi
+    buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi 
 cicMathView.cmx: matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
-    buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi
-lablGraphviz.cmo: lablGraphviz.cmi
-lablGraphviz.cmx: lablGraphviz.cmi
-matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
-matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
+    buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi 
+lablGraphviz.cmo: lablGraphviz.cmi 
+lablGraphviz.cmx: lablGraphviz.cmi 
+matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi 
+matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi 
 matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \
-    matitaEngine.cmi
+    matitaEngine.cmi 
 matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
-    matitaEngine.cmx
-matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
-matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
-matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
-matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
-matitaGeneratedGui.cmo:
-matitaGeneratedGui.cmx:
+    matitaEngine.cmx 
+matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi 
+matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi 
+matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi 
+matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi 
+matitaGeneratedGui.cmo: 
+matitaGeneratedGui.cmx: 
 matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \
-    matitaGtkMisc.cmi
+    matitaGtkMisc.cmi 
 matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
-    matitaGtkMisc.cmi
+    matitaGtkMisc.cmi 
 matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
     matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
-    matitaGeneratedGui.cmx matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi
+    matitaGeneratedGui.cmx matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi 
 matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
     matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
-    matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
-matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi
-matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
+    matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi 
+matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi 
+matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi 
 matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
     matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmx \
     matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmx \
-    applyTransformation.cmi matitaMathView.cmi
+    applyTransformation.cmi matitaMathView.cmi 
 matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
     matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \
     matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \
-    applyTransformation.cmx matitaMathView.cmi
-matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
-matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
+    applyTransformation.cmx matitaMathView.cmi 
+matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi 
+matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi 
 matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \
-    matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmx applyTransformation.cmi
+    matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmx applyTransformation.cmi 
 matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaInit.cmx \
-    matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx applyTransformation.cmx
+    matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx applyTransformation.cmx 
 matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
     matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \
-    buildTimeConf.cmx matitaScript.cmi
+    buildTimeConf.cmx matitaScript.cmi 
 matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
     matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \
-    buildTimeConf.cmx matitaScript.cmi
-matitaTypes.cmo: matitaTypes.cmi
-matitaTypes.cmx: matitaTypes.cmi
-predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi
-predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi
-virtuals.cmo: virtuals.cmi
-virtuals.cmx: virtuals.cmi
-applyTransformation.cmi:
-cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi
-lablGraphviz.cmi:
-matitaclean.cmi:
-matitaEngine.cmi: applyTransformation.cmi
-matitaExcPp.cmi:
-matitaGtkMisc.cmi: matitaGeneratedGui.cmx
-matitaGui.cmi: matitaGuiTypes.cmi
-matitaGuiTypes.cmi: matitaGeneratedGui.cmx applyTransformation.cmi
-matitaInit.cmi:
-matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
-matitaMisc.cmi: matitaGuiTypes.cmi
-matitaScript.cmi:
-matitaTypes.cmi:
-predefined_virtuals.cmi:
-virtuals.cmi:
+    buildTimeConf.cmx matitaScript.cmi 
+matitaTypes.cmo: matitaTypes.cmi 
+matitaTypes.cmx: matitaTypes.cmi 
+predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi 
+predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi 
+virtuals.cmo: virtuals.cmi 
+virtuals.cmx: virtuals.cmi 
+applyTransformation.cmi: 
+cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi 
+lablGraphviz.cmi: 
+matitaclean.cmi: 
+matitaEngine.cmi: applyTransformation.cmi 
+matitaExcPp.cmi: 
+matitaGtkMisc.cmi: matitaGeneratedGui.cmx 
+matitaGui.cmi: matitaGuiTypes.cmi 
+matitaGuiTypes.cmi: matitaGeneratedGui.cmx applyTransformation.cmi 
+matitaInit.cmi: 
+matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi 
+matitaMisc.cmi: matitaGuiTypes.cmi 
+matitaScript.cmi: 
+matitaTypes.cmi: 
+predefined_virtuals.cmi: 
+virtuals.cmi: