From: Ferruccio Guidi Date: Thu, 24 Nov 2011 19:26:24 +0000 (+0000) Subject: - now destruct tries to clear the replaced variables (from wilmer's X-Git-Tag: make_still_working~2063 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=432d0f324b7246c91f20545867c0da4bd25f588e;p=helm.git - 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 aec750131..34a327264 100644 --- 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 03a1732eb..5c11c1ded 100644 --- 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 fa6388aa7..9fdbeeeaf 100644 --- 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 b121fbcd1..6f707effc 100644 --- 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 301b9d8b8..64da37f13 100644 --- 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 fbe333cbd..3a2590d84 100644 --- 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 27787b008..d04ec9d2c 100644 --- 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 5142da1bf..e5cd5f2b3 100644 --- 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 28703386a..edb2abe95 100644 --- 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 1c8ec5b7c..dfb4400ff 100644 --- 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 b1a499fd3..fd1b831b9 100644 --- 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 d5306074a..0810bc8be 100644 --- 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 c57bf8efe..5e4dabb6a 100644 --- 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 b9e7731f9..48127a325 100644 --- 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 f6eae06d6..2e31be0ec 100644 --- 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 5e055ecdc..2633e1aba 100644 --- 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 47f203f0a..c85683251 100644 --- 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 3e01ca0fb..c85683251 100644 --- 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 12a1efd7e..c9e46dc2a 100644 --- 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 19a1fd325..40c03891a 100644 --- 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 119f13093..25e67131f 100644 --- 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 8f195d05a..3d7dfc21f 100644 --- 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 e25145b8b..6616a03d0 100644 --- 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 eda62779f..e7e7ffbd7 100644 --- 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 fb48e954c..74d8be432 100644 --- 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: