-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-helmLogger.cmi:
-helmLogger.cmo: helmLogger.cmi
-helmLogger.cmx: helmLogger.cmi
+helmLogger.cmi:
+helmLogger.cmo: helmLogger.cmi
+helmLogger.cmx: helmLogger.cmi
-helmLogger.cmi:
-helmLogger.cmo: helmLogger.cmi
-helmLogger.cmx: helmLogger.cmi
+helmLogger.cmi:
+helmLogger.cmo: helmLogger.cmi
+helmLogger.cmx: helmLogger.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
+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
+ncic2astMatcher.cmi:
+interpretations.cmi:
+ncic2astMatcher.cmo: ncic2astMatcher.cmi
+ncic2astMatcher.cmx: ncic2astMatcher.cmi
+interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi
+interpretations.cmx: ncic2astMatcher.cmx interpretations.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
+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
-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
-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
-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
-nCicLibrary.cmi:
-nCicLibrary.cmo: nCicLibrary.cmi
-nCicLibrary.cmx: nCicLibrary.cmi
+nCicLibrary.cmi:
+nCicLibrary.cmo: nCicLibrary.cmi
+nCicLibrary.cmx: nCicLibrary.cmi
-nCicLibrary.cmi:
-nCicLibrary.cmo: nCicLibrary.cmi
-nCicLibrary.cmx: nCicLibrary.cmi
+nCicLibrary.cmi:
+nCicLibrary.cmo: nCicLibrary.cmi
+nCicLibrary.cmx: nCicLibrary.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
+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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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
-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:
-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:
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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)
+.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
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
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)
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 }.
(* *)
(**************************************************************************)
-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 // <minus_n_n
->(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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
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).
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.
;;
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"; "๐ก"; "โจ"; ] ;
]
;;
projects / helm.git / commitdiff