From b5a168bec5e813258c510a1f2a00ce9f57ecee5a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 7 Jan 2012 19:29:46 +0000 Subject: [PATCH] lambda_delta: global environments handling: redefined and first results rtm: first definitions lib/arithmetics/nat: a missing lemma added predefined_virtuals: we added circled numbers, circled letters and other characters depend, depend.opt: regenerated --- matita/components/content/.depend | 28 ++-- matita/components/content/.depend.opt | 28 ++-- matita/components/content_pres/.depend | 60 ++++---- matita/components/content_pres/.depend.opt | 60 ++++---- matita/components/disambiguation/.depend | 18 +-- matita/components/disambiguation/.depend.opt | 18 +-- matita/components/extlib/.depend | 54 ++++---- matita/components/extlib/.depend.opt | 54 ++++---- matita/components/getter/.depend | 52 +++---- matita/components/getter/.depend.opt | 52 +++---- matita/components/grafite/.depend | 10 +- matita/components/grafite/.depend.opt | 10 +- matita/components/grafite_engine/.depend | 18 +-- matita/components/grafite_engine/.depend.opt | 18 +-- matita/components/grafite_parser/.depend | 12 +- matita/components/grafite_parser/.depend.opt | 12 +- matita/components/library/.depend | 18 +-- matita/components/library/.depend.opt | 18 +-- matita/components/logger/.depend | 6 +- matita/components/logger/.depend.opt | 6 +- matita/components/ng_cic_content/.depend | 12 +- matita/components/ng_cic_content/.depend.opt | 12 +- matita/components/ng_disambiguation/.depend | 24 ++-- .../components/ng_disambiguation/.depend.opt | 24 ++-- matita/components/ng_kernel/.depend | 58 ++++---- matita/components/ng_kernel/.depend.opt | 58 ++++---- matita/components/ng_library/.depend | 6 +- matita/components/ng_library/.depend.opt | 6 +- matita/components/ng_paramodulation/.depend | 78 +++++------ .../components/ng_paramodulation/.depend.opt | 78 +++++------ matita/components/ng_refiner/.depend | 42 +++--- matita/components/ng_refiner/.depend.opt | 42 +++--- matita/components/ng_tactics/.depend | 48 +++---- matita/components/ng_tactics/.depend.opt | 48 +++---- matita/components/registry/.depend | 6 +- matita/components/registry/.depend.opt | 6 +- matita/components/syntax_extensions/.depend | 10 +- .../components/syntax_extensions/.depend.opt | 10 +- matita/components/thread/.depend | 12 +- matita/components/thread/.depend.opt | 12 +- matita/components/xml/.depend | 12 +- matita/components/xml/.depend.opt | 12 +- matita/matita/.depend | 108 +++++++-------- matita/matita/.depend.opt | 108 +++++++-------- .../lambda_delta/Basic_2/functional/rtm.ma | 85 ++++++++++++ .../Basic_2/functional/rtm_step.ma | 54 ++++++++ .../lambda_delta/Basic_2/grammar/genv.ma | 31 +++++ .../contribs/lambda_delta/Basic_2/names.txt | 9 +- .../contribs/lambda_delta/Basic_2/notation.ma | 4 + .../Basic_2/substitution/gdrop.ma | 76 ++++++++--- .../Basic_2/substitution/gdrop_gdrop.ma | 40 ++++++ .../contribs/lambda_delta/Ground_2/list.ma | 8 ++ matita/matita/lib/arithmetics/nat.ma | 3 + matita/matita/predefined_virtuals.ml | 128 +++++++++--------- 54 files changed, 1042 insertions(+), 780 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma diff --git a/matita/components/content/.depend b/matita/components/content/.depend index f4b4f3037..0671b66fe 100644 --- a/matita/components/content/.depend +++ b/matita/components/content/.depend @@ -1,14 +1,14 @@ -content.cmi: -notationUtil.cmi: notationPt.cmo -notationEnv.cmi: notationPt.cmo -notationPp.cmi: notationPt.cmo notationEnv.cmi -notationPt.cmo: -notationPt.cmx: -content.cmo: content.cmi -content.cmx: content.cmi -notationUtil.cmo: notationPt.cmo notationUtil.cmi -notationUtil.cmx: notationPt.cmx notationUtil.cmi -notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi -notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi -notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi -notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi +content.cmi: +notationUtil.cmi: notationPt.cmo +notationEnv.cmi: notationPt.cmo +notationPp.cmi: notationPt.cmo notationEnv.cmi +notationPt.cmo: +notationPt.cmx: +content.cmo: content.cmi +content.cmx: content.cmi +notationUtil.cmo: notationPt.cmo notationUtil.cmi +notationUtil.cmx: notationPt.cmx notationUtil.cmi +notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi +notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi +notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi +notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index 34a327264..aec750131 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 b/matita/components/content_pres/.depend index 5c11c1ded..03a1732eb 100644 --- a/matita/components/content_pres/.depend +++ b/matita/components/content_pres/.depend @@ -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/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt index 5c11c1ded..03a1732eb 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 b/matita/components/disambiguation/.depend index 9fdbeeeaf..fa6388aa7 100644 --- a/matita/components/disambiguation/.depend +++ b/matita/components/disambiguation/.depend @@ -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/disambiguation/.depend.opt b/matita/components/disambiguation/.depend.opt index 9fdbeeeaf..fa6388aa7 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 b/matita/components/extlib/.depend index 6f707effc..b121fbcd1 100644 --- a/matita/components/extlib/.depend +++ b/matita/components/extlib/.depend @@ -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/extlib/.depend.opt b/matita/components/extlib/.depend.opt index 6f707effc..b121fbcd1 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 b/matita/components/getter/.depend index ca64d8ec0..600dc01db 100644 --- a/matita/components/getter/.depend +++ b/matita/components/getter/.depend @@ -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.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 -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.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 +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.cmo 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.cmo \ - 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.cmo 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.cmo \ 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/getter/.depend.opt b/matita/components/getter/.depend.opt index 64da37f13..301b9d8b8 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 b/matita/components/grafite/.depend index 0e7eba453..ba4fab03a 100644 --- a/matita/components/grafite/.depend +++ b/matita/components/grafite/.depend @@ -1,5 +1,5 @@ -grafiteAstPp.cmi: grafiteAst.cmo -grafiteAst.cmo: -grafiteAst.cmx: -grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi -grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi +grafiteAstPp.cmi: grafiteAst.cmo +grafiteAst.cmo: +grafiteAst.cmx: +grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi +grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi diff --git a/matita/components/grafite/.depend.opt b/matita/components/grafite/.depend.opt index 3a2590d84..fbe333cbd 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 b/matita/components/grafite_engine/.depend index d04ec9d2c..27787b008 100644 --- a/matita/components/grafite_engine/.depend +++ b/matita/components/grafite_engine/.depend @@ -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_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt index d04ec9d2c..27787b008 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 b/matita/components/grafite_parser/.depend index e5cd5f2b3..5142da1bf 100644 --- a/matita/components/grafite_parser/.depend +++ b/matita/components/grafite_parser/.depend @@ -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/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index e5cd5f2b3..5142da1bf 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 b/matita/components/library/.depend index edb2abe95..28703386a 100644 --- a/matita/components/library/.depend +++ b/matita/components/library/.depend @@ -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/library/.depend.opt b/matita/components/library/.depend.opt index edb2abe95..28703386a 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 b/matita/components/logger/.depend index dfb4400ff..1c8ec5b7c 100644 --- a/matita/components/logger/.depend +++ b/matita/components/logger/.depend @@ -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/logger/.depend.opt b/matita/components/logger/.depend.opt index dfb4400ff..1c8ec5b7c 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 b/matita/components/ng_cic_content/.depend index fd1b831b9..b1a499fd3 100644 --- a/matita/components/ng_cic_content/.depend +++ b/matita/components/ng_cic_content/.depend @@ -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_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt index fd1b831b9..b1a499fd3 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 b/matita/components/ng_disambiguation/.depend index 0810bc8be..d5306074a 100644 --- a/matita/components/ng_disambiguation/.depend +++ b/matita/components/ng_disambiguation/.depend @@ -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_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt index 0810bc8be..d5306074a 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 b/matita/components/ng_kernel/.depend index 0bf995539..16f0d02cc 100644 --- a/matita/components/ng_kernel/.depend +++ b/matita/components/ng_kernel/.depend @@ -1,41 +1,41 @@ -nUri.cmi: -nReference.cmi: nUri.cmi -nCicUtils.cmi: nCic.cmo -nCicSubstitution.cmi: nCic.cmo -nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo -nCicReduction.cmi: nCic.cmo -nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo -nCicUntrusted.cmi: nCic.cmo -nCicPp.cmi: nReference.cmi nCic.cmo -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.cmo nCicUtils.cmi -nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi +nUri.cmi: +nReference.cmi: nUri.cmi +nCicUtils.cmi: nCic.cmo +nCicSubstitution.cmi: nCic.cmo +nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo +nCicReduction.cmi: nCic.cmo +nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo +nCicUntrusted.cmi: nCic.cmo +nCicPp.cmi: nReference.cmi nCic.cmo +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.cmo nCicUtils.cmi +nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmo \ - nCicSubstitution.cmi + nCicSubstitution.cmi nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \ - nCicSubstitution.cmi -nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi -nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi + nCicSubstitution.cmi +nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi +nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicEnvironment.cmi nCic.cmo nCicReduction.cmi + nCicEnvironment.cmi nCic.cmo 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.cmo \ - 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.cmo nCicUntrusted.cmi + nCicReduction.cmi nCicEnvironment.cmi nCic.cmo 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.cmo nCicPp.cmi + nCicEnvironment.cmi nCic.cmo 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_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt index 5e4dabb6a..c57bf8efe 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 b/matita/components/ng_library/.depend index 48127a325..b9e7731f9 100644 --- a/matita/components/ng_library/.depend +++ b/matita/components/ng_library/.depend @@ -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_library/.depend.opt b/matita/components/ng_library/.depend.opt index 48127a325..b9e7731f9 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 b/matita/components/ng_paramodulation/.depend index 2e31be0ec..f6eae06d6 100644 --- a/matita/components/ng_paramodulation/.depend +++ b/matita/components/ng_paramodulation/.depend @@ -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_paramodulation/.depend.opt b/matita/components/ng_paramodulation/.depend.opt index 2e31be0ec..f6eae06d6 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 b/matita/components/ng_refiner/.depend index 2633e1aba..5e055ecdc 100644 --- a/matita/components/ng_refiner/.depend +++ b/matita/components/ng_refiner/.depend @@ -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_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt index 2633e1aba..5e055ecdc 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 c85683251..3e01ca0fb 100644 --- a/matita/components/ng_tactics/.depend +++ b/matita/components/ng_tactics/.depend @@ -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/.depend.opt b/matita/components/ng_tactics/.depend.opt index c85683251..3e01ca0fb 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/registry/.depend b/matita/components/registry/.depend index 40c03891a..19a1fd325 100644 --- a/matita/components/registry/.depend +++ b/matita/components/registry/.depend @@ -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/registry/.depend.opt b/matita/components/registry/.depend.opt index 40c03891a..19a1fd325 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 25e67131f..119f13093 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 3d7dfc21f..8f195d05a 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 b/matita/components/thread/.depend index 6616a03d0..e25145b8b 100644 --- a/matita/components/thread/.depend +++ b/matita/components/thread/.depend @@ -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/thread/.depend.opt b/matita/components/thread/.depend.opt index 6616a03d0..e25145b8b 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 b/matita/components/xml/.depend index e7e7ffbd7..eda62779f 100644 --- a/matita/components/xml/.depend +++ b/matita/components/xml/.depend @@ -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/components/xml/.depend.opt b/matita/components/xml/.depend.opt index e7e7ffbd7..eda62779f 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 b/matita/matita/.depend index 8325fc357..c63191cf0 100644 --- a/matita/matita/.depend +++ b/matita/matita/.depend @@ -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.cmo applyTransformation.cmi cicMathView.cmi + buildTimeConf.cmo 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.cmo buildTimeConf.cmo \ - 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.cmo matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi + matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmo 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.cmo matitaInit.cmi -matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi + matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi +matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi +matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \ matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmo \ - 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.cmo matitaMisc.cmi -matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi + applyTransformation.cmx matitaMathView.cmi +matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi +matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \ - matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo applyTransformation.cmi + matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo 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.cmo matitaScript.cmi + buildTimeConf.cmo 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.cmo -matitaGui.cmi: matitaGuiTypes.cmi -matitaGuiTypes.cmi: matitaGeneratedGui.cmo 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.cmo +matitaGui.cmi: matitaGuiTypes.cmi +matitaGuiTypes.cmi: matitaGeneratedGui.cmo applyTransformation.cmi +matitaInit.cmi: +matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi +matitaMisc.cmi: matitaGuiTypes.cmi +matitaScript.cmi: +matitaTypes.cmi: +predefined_virtuals.cmi: +virtuals.cmi: diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index 74d8be432..fb48e954c 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: diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma new file mode 100644 index 000000000..b15db8653 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma @@ -0,0 +1,85 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/grammar/term_vector.ma". +include "Basic_2/grammar/genv.ma". + +(* REDUCTION AND TYPE MACHINE ***********************************************) + +(* machine local environment *) +inductive xenv: Type[0] ≝ +| XAtom: xenv (* empty *) +| XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *) +. + +interpretation "atom (ext. local environment)" + 'Star = XAtom. + +interpretation "environment binding construction (quad)" + 'DBind L I u K V = (XQuad L I u K V). + +(* machine stack *) +definition stack: Type[0] ≝ list2 xenv term. + +(* machine status *) +record rtm: Type[0] ≝ +{ rg: genv; (* global environment *) + ru: nat; (* current de Bruijn's level *) + re: xenv; (* extended local environment *) + rs: stack; (* application stack *) + rt: term (* code *) +}. + +(* initial state *) +definition rtm_i: genv → term → rtm ≝ + λG,T. mk_rtm G 0 (⋆) (⟠) T. + +(* update code *) +definition rtm_t: rtm → term → rtm ≝ + λM,T. match M with + [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (⟠) T + ]. + +(* update closure *) +definition rtm_u: rtm → xenv → term → rtm ≝ + λM,E,T. match M with + [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (⟠) T + ]. + +(* get global environment *) +definition rtm_g: rtm → genv ≝ + λM. match M with + [ mk_rtm G _ _ _ _ ⇒ G + ]. + +(* get local reference level *) +definition rtm_l: rtm → nat ≝ + λM. match M with + [ mk_rtm _ u E _ _ ⇒ match E with + [ XAtom ⇒ u + | XQuad _ _ u _ _ ⇒ u + ] + ]. + +(* get stack *) +definition rtm_s: rtm → stack ≝ + λM. match M with + [ mk_rtm _ _ _ S _ ⇒ S + ]. + +(* get code *) +definition rtm_c: rtm → term ≝ + λM. match M with + [ mk_rtm _ _ _ _ T ⇒ T + ]. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma new file mode 100644 index 000000000..470288882 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/functional/rtm.ma". + +(* REDUCTION AND TYPE MACHINE ***********************************************) + +(* transitions *) +inductive rtm_step: relation rtm ≝ +| rtm_ldrop : ∀G,u,E,I,t,F,V,S,i. + rtm_step (mk_rtm G u (E. ④{I} {t, F, V}) S (#(i + 1))) + (mk_rtm G u E S (#i)) +| rtm_ldelta: ∀G,u,E,t,F,V,S. + rtm_step (mk_rtm G u (E. ④{Abbr} {t, F, V}) S (#0)) + (mk_rtm G u F S V) +| rtm_ltype : ∀G,u,E,t,F,V,S. + rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0)) + (mk_rtm G u F S V) +| rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| → + rtm_step (mk_rtm (G. 𝕓{I} V) u E S (§p)) + (mk_rtm G u E S (§p)) +| rtm_gdelta: ∀G,V,u,E,S,p. p = |G| → + rtm_step (mk_rtm (G. 𝕓{Abbr} V) u E S (§p)) + (mk_rtm G u E S V) +| rtm_gtype : ∀G,V,u,E,S,p. p = |G| → + rtm_step (mk_rtm (G. 𝕓{Abst} V) u E S (§p)) + (mk_rtm G u E S V) +| rtm_tau : ∀G,u,E,S,W,T. + rtm_step (mk_rtm G u E S (𝕔{Cast} W. T)) + (mk_rtm G u E S T) +| rtm_appl : ∀G,u,E,S,V,T. + rtm_step (mk_rtm G u E S (𝕔{Appl} V. T)) + (mk_rtm G u E ({E, V} :: S) T) +| rtm_beta : ∀G,u,E,F,V,S,W,T. + rtm_step (mk_rtm G u E ({F, V} :: S) (𝕔{Abst} W. T)) + (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T) +| rtm_push : ∀G,u,E,W,T. + rtm_step (mk_rtm G u E ⟠ (𝕔{Abst} W. T)) + (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T) +| rtm_theta : ∀G,u,E,S,V,T. + rtm_step (mk_rtm G u E S (𝕔{Abbr} V. T)) + (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) +. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma new file mode 100644 index 000000000..dad4fd230 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Ground_2/list.ma". +include "Basic_2/grammar/term.ma". + +(* GLOBAL ENVIRONMENTS ******************************************************) + +(* global environments *) +definition genv ≝ list2 bind2 term. + +interpretation "sort (global environment)" + 'Star = (nil2 bind2 term). + +interpretation "environment binding construction (binary)" + 'DBind L I T = (cons2 bind2 term I T L). + +(* Basic properties *********************************************************) + +axiom genv_eq_dec: ∀T1,T2:genv. Decidable (T1 = T2). diff --git a/matita/matita/contribs/lambda_delta/Basic_2/names.txt b/matita/matita/contribs/lambda_delta/Basic_2/names.txt index 9078f4aef..a57d3affb 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/names.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/names.txt @@ -2,16 +2,17 @@ NAMING CONVENTIONS FOR METAVARIABLES A,B : arity C,D : candidate of reducibility -E,F,G : reserved: future use +E,F : RTM environment +G : global environment H : reserved: transient premise IH : reserved: inductive premise I,J : item K,L : local environment M,N : reserved: future use -O : reserved: standard library +O : P,Q : reserved: future use R : generic predicate (relation) -S : reserved: standard library +S : RTM stack T,U,V,W: term X,Y,Z : reserved: transient objet denoted by a capital letter @@ -21,4 +22,4 @@ h : sort hierarchy parameter i,j : local reference position index (de Bruijn's) k : sort index p,q : global reference position - +t,u : local reference position level (de Bruijn's) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 36f9f7652..f528a9062 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -68,6 +68,10 @@ notation > "hvbox( T . break 𝕔 { I } break term 90 T1 )" non associative with precedence 89 for @{ 'DBind $T $I $T1 }. *) (**) (* this breaks all parsing *) +notation "hvbox( T . break ④ { I } break { T1 , break T2 , break T3 } )" + non associative with precedence 47 + for @{ 'DBind $T $I $T1 $T2 $T3 }. + notation "hvbox( # [ x ] )" non associative with precedence 90 for @{ 'Weight $x }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma index 5cef64937..2f677cb2f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma @@ -12,33 +12,69 @@ (* *) (**************************************************************************) -include "Basic_2/substitution/ldrop.ma". +include "Basic_2/grammar/genv.ma". (* GLOBAL ENVIRONMENT SLICING ***********************************************) -inductive gdrop (e:nat) (G1:lenv) : predicate lenv ≝ -| gdrop_lt: ∀G2. e < |G1| → ⇓[0, |G1| - (e + 1)] G1 ≡ G2 → gdrop e G1 G2 -| gdrop_ge: |G1| ≤ e → gdrop e G1 (⋆) +inductive gdrop (e:nat): relation genv ≝ +| gdrop_gt: ∀G. |G| ≤ e → gdrop e G (⋆) +| gdrop_eq: ∀G. |G| = e + 1 → gdrop e G G +| gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. 𝕓{I} V) G2 . -interpretation "global slicing" 'RGDrop e G1 G2 = (gdrop e G1 G2). +interpretation "global slicing" + 'RLDrop e G1 G2 = (gdrop e G1 G2). (* basic inversion lemmas ***************************************************) -(* -fact gdrop_inv_atom2_aux: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → G2 = ⋆ → |G1| ≤ e. -#G1 #G2 #e * -G2 // -#G2 #He #HG12 #H destruct -lapply (ldrop_fwd_O1_length … HG12) -HG12 ->minus_le_minus_minus_comm // -He >le_plus_minus_comm // (commutative_plus e) normalize #H destruct -qed. -lemma gdrop_inv_atom2: ∀G1,e. ⇓[e] G1 ≡ ⋆ → |G1| ≤ e. -/2 width=3/ qed-. +lemma gdrop_inv_gt: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆. +#G1 #G2 #e * -G1 -G2 // +[ #G #H >H -H >commutative_plus #H + lapply (le_plus_to_le_r … 0 H) -H #H + lapply (le_n_O_to_eq … H) -H #H destruct +| #I #G1 #G2 #V #H1 #_ #H2 + lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 normalize in ⊢ (? % ? → ?); >commutative_plus #H + lapply (lt_plus_to_lt_l … 0 H) -H #H + elim (lt_zero_false … H) +] +qed-. -lemma gdrop_inv_ge: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆. -#G1 #G2 #e * // #G2 #H1 #_ #H2 -lapply (lt_to_le_to_lt … H1 H2) -H1 -H2 #He -elim (lt_refl_false … He) +lemma gdrop_inv_eq: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2. +#G1 #G2 #e * -G1 -G2 // +[ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H + lapply (le_plus_to_le_r … 0 H) -H #H + lapply (le_n_O_to_eq … H) -H #H destruct +| #I #G1 #G2 #V #H1 #_ normalize #H2 + <(injective_plus_l … H2) in H1; -H2 #H + elim (lt_refl_false … H) +] qed-. -*) + +fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇓[e] G ≡ G2 → G = G1. 𝕓{I} V → + e < |G1| → ⇓[e] G1 ≡ G2. +#I #G #G1 #G2 #V #e * -G -G2 +[ #G #H1 #H destruct #H2 + lapply (le_to_lt_to_lt … H1 H2) -H1 -H2 normalize in ⊢ (? % ? → ?); >commutative_plus #H + lapply (lt_plus_to_lt_l … 0 H) -H #H + elim (lt_zero_false … H) +| #G #H1 #H2 destruct >(injective_plus_l … H1) -H1 #H + elim (lt_refl_false … H) +| #J #G #G2 #W #_ #HG2 #H destruct // +] +qed. + +lemma gdrop_inv_lt: ∀I,G1,G2,V,e. + ⇓[e] G1. 𝕓{I} V ≡ G2 → e < |G1| → ⇓[e] G1 ≡ G2. +/2 width=5/ qed-. + +(* Basic properties *********************************************************) + +lemma gdrop_total: ∀e,G1. ∃G2. ⇓[e] G1 ≡ G2. +#e #G1 elim G1 -G1 /3 width=2/ +#I #V #G1 * #G2 #HG12 +elim (lt_or_eq_or_gt e (|G1|)) #He +[ /3 width=2/ +| destruct /3 width=2/ +| @ex_intro [2: @gdrop_gt normalize /2 width=1/ | skip ] (**) (* explicit constructor *) +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma new file mode 100644 index 000000000..9083e2b3a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Basic_2/substitution/gdrop.ma". + +(* GLOBAL ENVIRONMENT SLICING ***********************************************) + +(* Main properties **********************************************************) + +theorem gdrop_mono: ∀G,G1,e. ⇓[e] G ≡ G1 → ∀G2. ⇓[e] G ≡ G2 → G1 = G2. +#G #G1 #e #H elim H -G -G1 +[ #G #He #G2 #H + >(gdrop_inv_gt … H He) -H -He // +| #G #He #G2 #H + >(gdrop_inv_eq … H He) -H -He // +| #I #G #G1 #V #He #_ #IHG1 #G2 #H + lapply (gdrop_inv_lt … H He) -H -He /2 width=1/ +] +qed-. + +lemma gdrop_dec: ∀G1,G2,e. Decidable (⇓[e] G1 ≡ G2). +#G1 #G2 #e +elim (gdrop_total e G1) #G #HG1 +elim (genv_eq_dec G G2) #HG2 +[ destruct /2 width=1/ +| @or_intror #HG12 + lapply (gdrop_mono … HG1 … HG12) -HG1 -HG12 /2 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma index 09a52f57d..883a8a8ba 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma @@ -45,3 +45,11 @@ let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with interpretation "append (list of pairs)" 'Append l1 l2 = (append2 ? ? l1 l2). + +let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with +[ nil2 ⇒ 0 +| cons2 _ _ l ⇒ length2 A1 A2 l + 1 +]. + +interpretation "length (list of pairs)" + 'card l = (length2 ? ? l). diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 8f7acf2b2..44c3119fa 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -132,6 +132,9 @@ theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a. theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m). #n (elim n) normalize /3/ qed. +theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n). +/2/ qed. + theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m. /2/ qed. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 49d5f866d..c14fe8ace 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,7 +1503,7 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ - ["→"; "⇉"; "⇒"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; "⥤"; "⥰"; ] ; + ["→"; "⇉"; "⇒"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; "⥤"; "⥰"; "➾"; ] ; ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ]; ["_" ; "⎽"; "⎼"; "⎻"; "⎺"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰";] ; @@ -1512,70 +1512,70 @@ let predefined_classes = [ ["{"; "❴";]; ["}"; "❵";]; ["□"; "◽"; "▪"; "◾"; ]; - ["◊"; "♢"; "⧫"; "♦"; ]; + ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ]; [">"; "〉"; "»"; "❭"; "❯"; "❱"; ]; - ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; ] ; - ["A"; "ℵ"; "𝔸"; "𝐀";] ; - ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; ] ; - ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁";] ; - ["c"; "𝕔"; "𝐜";] ; - ["C"; "ℭ"; "∁"; "𝐂";] ; - ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅";] ; - ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; ] ; - ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; ] ; - ["E"; "ℰ"; "𝔼"; "𝐄";] ; - ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛟"; "𝛙"; ] ; - ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; ] ; - ["g"; "γ"; "ℊ"; "𝕘"; "𝐠"; "𝛄"; ] ; - ["G"; "Γ"; "𝔾"; "𝐆"; "𝚪"; ] ; - ["h"; "η"; "ℌ"; "ℎ"; "𝕙"; "𝐡";] ; - ["H"; "ℋ"; "ℍ"; "𝐇";] ; - ["i"; "ι"; "ℐ"; "𝕚"; "ⅈ"; "𝐢"; "𝛊"; ] ; - ["I"; "𝕀"; "𝐈";] ; - ["j"; "𝕛"; "𝐣";] ; - ["J"; "Ј"; "𝕁"; "𝐉";] ; - ["k"; "κ"; "𝕜"; "𝐤"; "𝛋"; ] ; - ["K"; "𝕂"; "𝐊"; ] ; - ["l"; "λ"; "𝕝"; "𝐥"; "𝛌"; ] ; - ["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; ] ; - ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; ] ; - ["M"; "ℳ"; "𝕄"; "𝐌"; ] ; - ["n"; "𝕟"; "𝐧"; "𝛈"; ] ; - ["N"; "ℕ"; "№"; "𝐍";] ; - ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "ø"; "○"; "𝐨"; "𝛉"; ] ; - ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹";] ; - ["p"; "π"; "𝕡"; "𝐩"; "𝛑";] ; - ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; ] ; - ["q"; "𝕢"; "𝐪";] ; - ["Q"; "ℚ"; "𝐐";] ; - ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; ] ; - ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑";] ; - ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; ] ; - ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; ] ; - ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; ] ; - ["T"; "𝕋"; "𝐓";] ; - ["u"; "𝕦"; "𝐮";] ; - ["U"; "𝕌"; "𝐔"; ] ; - ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; ] ; - ["V"; "𝕍"; "𝐕";] ; - ["w"; "ω"; "𝕨"; "𝐰"; "𝛚"; ] ; - ["W"; "Ω"; "𝕎"; "𝐖"; "𝛀"; ] ; - ["x"; "ξ"; "χ"; "ϰ"; "𝕩"; "𝐱"; "𝛏"; "𝛘"; "𝛞"; ] ; - ["X"; "Ξ"; "𝕏";"𝐗"; "𝚵"; ] ; - ["y"; "υ"; "𝕪"; "𝐲";] ; - ["Y"; "ϒ"; "𝕐"; "𝐘"; "𝚼"; ] ; - ["z"; "ζ"; "𝕫"; "𝐳"; "𝛇"; ] ; - ["Z"; "ℨ"; "ℤ"; "𝐙";] ; - ["0"; "𝟘"; ] ; - ["1"; "𝟙"; ] ; - ["2"; "𝟚"; ] ; - ["3"; "𝟛"; ] ; - ["4"; "𝟜"; ] ; - ["5"; "𝟝"; ] ; - ["6"; "𝟞"; ] ; - ["7"; "𝟟"; ] ; - ["8"; "𝟠"; ] ; - ["9"; "𝟡"; ] ; + ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; + ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; + ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; + ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ; + ["c"; "𝕔"; "𝐜"; "ⓒ"; ] ; + ["C"; "ℭ"; "∁"; "𝐂"; "Ⓒ"; ] ; + ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅"; "ⓓ"; ] ; + ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; ] ; + ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ; + ["E"; "ℰ"; "𝔼"; "𝐄"; "Ⓔ"; ] ; + ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛟"; "𝛙"; "ⓕ"; ] ; + ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; ] ; + ["g"; "γ"; "ℊ"; "𝕘"; "𝐠"; "𝛄"; "ⓖ"; ] ; + ["G"; "Γ"; "𝔾"; "𝐆"; "𝚪"; "Ⓖ"; ] ; + ["h"; "η"; "ℌ"; "ℎ"; "𝕙"; "𝐡"; "ⓗ"; ] ; + ["H"; "ℋ"; "ℍ"; "𝐇"; "Ⓗ"; ] ; + ["i"; "ι"; "ℐ"; "𝕚"; "ⅈ"; "𝐢"; "𝛊"; "ⓘ"; ] ; + ["I"; "𝕀"; "𝐈"; "Ⓘ"; ] ; + ["j"; "𝕛"; "𝐣"; "ⓙ"; ] ; + ["J"; "Ј"; "𝕁"; "𝐉"; "Ⓙ"; ] ; + ["k"; "κ"; "𝕜"; "𝐤"; "𝛋"; "ⓚ"; ] ; + ["K"; "𝕂"; "𝐊"; "Ⓚ"; ] ; + ["l"; "λ"; "𝕝"; "𝐥"; "𝛌"; "ⓛ"; ] ; + ["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; "Ⓛ"; ] ; + ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; ] ; + ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ; + ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ; + ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ; + ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ; + ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ; + ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ; + ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ; + ["q"; "𝕢"; "𝐪"; "ⓠ"; ] ; + ["Q"; "ℚ"; "𝐐"; "Ⓠ"; ] ; + ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ; + ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; ] ; + ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ; + ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; ] ; + ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ; + ["T"; "𝕋"; "𝐓"; "Ⓣ"; ] ; + ["u"; "𝕦"; "𝐮"; "ⓤ"; ] ; + ["U"; "𝕌"; "𝐔"; "Ⓤ"; ] ; + ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; ] ; + ["V"; "𝕍"; "𝐕"; "Ⓥ"; ] ; + ["w"; "ω"; "𝕨"; "𝐰"; "𝛚"; "ⓦ"; ] ; + ["W"; "Ω"; "𝕎"; "𝐖"; "𝛀"; "Ⓦ"; ] ; + ["x"; "ξ"; "χ"; "ϰ"; "𝕩"; "𝐱"; "𝛏"; "𝛘"; "𝛞"; "ⓧ"; ] ; + ["X"; "Ξ"; "𝕏";"𝐗"; "𝚵"; "Ⓧ"; ] ; + ["y"; "υ"; "𝕪"; "𝐲"; "ⓨ"; ] ; + ["Y"; "ϒ"; "𝕐"; "𝐘"; "𝚼"; "Ⓨ"; ] ; + ["z"; "ζ"; "𝕫"; "𝐳"; "𝛇"; "ⓩ"; ] ; + ["Z"; "ℨ"; "ℤ"; "𝐙"; "Ⓩ"; ] ; + ["0"; "𝟘"; "⓪"; ] ; + ["1"; "𝟙"; "①"; ] ; + ["2"; "𝟚"; "②"; ] ; + ["3"; "𝟛"; "③"; ] ; + ["4"; "𝟜"; "④"; ] ; + ["5"; "𝟝"; "⑤"; ] ; + ["6"; "𝟞"; "⑥"; ] ; + ["7"; "𝟟"; "⑦"; ] ; + ["8"; "𝟠"; "⑧"; ] ; + ["9"; "𝟡"; "⑨"; ] ; ] ;; -- 2.39.2