- content.cmo : content.cmi
- content.cmx : content.cmi
++content.cmo : \
++ content.cmi
++content.cmx : \
++ content.cmi
content.cmi :
- notationEnv.cmo : notationUtil.cmi notationPt.cmo notationEnv.cmi
- notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationUtil.cmi : notationPt.cmo
--notationEnv.cmi : notationPt.cmo
- notationPp.cmo : notationPt.cmo notationEnv.cmi notationPp.cmi
- notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi
--notationPp.cmi : notationPt.cmo notationEnv.cmi
++notationEnv.cmo : \
++ notationUtil.cmi \
++ notationPt.cmo \
++ notationEnv.cmi
++notationEnv.cmx : \
++ notationUtil.cmx \
++ notationPt.cmx \
++ notationEnv.cmi
++notationEnv.cmi : \
++ notationPt.cmo
++notationPp.cmo : \
++ notationPt.cmo \
++ notationEnv.cmi \
++ notationPp.cmi
++notationPp.cmx : \
++ notationPt.cmx \
++ notationEnv.cmx \
++ notationPp.cmi
++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
- notationUtil.cmi : notationPt.cmo
-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
++notationUtil.cmo : \
++ notationPt.cmo \
++ notationUtil.cmi
++notationUtil.cmx : \
++ notationPt.cmx \
++ notationUtil.cmi
++notationUtil.cmi : \
++ notationPt.cmo
- content.cmx : content.cmi
++content.cmx : \
++ content.cmi
content.cmi :
- notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationUtil.cmi : notationPt.cmx
--notationEnv.cmi : notationPt.cmx
- notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi
--notationPp.cmi : notationPt.cmx notationEnv.cmi
-notationPt.cmo :
++notationEnv.cmx : \
++ notationUtil.cmx \
++ notationPt.cmx \
++ notationEnv.cmi
++notationEnv.cmi : \
++ notationPt.cmx
++notationPp.cmx : \
++ notationPt.cmx \
++ notationEnv.cmx \
++ notationPp.cmi
++notationPp.cmi : \
++ notationPt.cmx \
++ notationEnv.cmi
notationPt.cmx :
-content.cmo : content.cmi
-content.cmx : content.cmi
-notationUtil.cmo : notationPt.cmx notationUtil.cmi
--notationUtil.cmx : notationPt.cmx notationUtil.cmi
- notationUtil.cmi : notationPt.cmx
-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
++notationUtil.cmx : \
++ notationPt.cmx \
++ notationUtil.cmi
++notationUtil.cmi : \
++ notationPt.cmx
- box.cmo : renderingAttrs.cmi box.cmi
- box.cmx : renderingAttrs.cmx box.cmi
-renderingAttrs.cmi :
-cicNotationLexer.cmi :
-cicNotationParser.cmi :
-mpresentation.cmi :
++box.cmo : \
++ renderingAttrs.cmi \
++ box.cmi
++box.cmx : \
++ renderingAttrs.cmx \
++ box.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
-termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
--boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
++boxPp.cmo : \
++ renderingAttrs.cmi \
++ mpresentation.cmi \
++ cicNotationPres.cmi \
++ box.cmi \
boxPp.cmi
--boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
++boxPp.cmx : \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ cicNotationPres.cmx \
++ box.cmx \
boxPp.cmi
- boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi
- cicNotationLexer.cmo : cicNotationLexer.cmi
- cicNotationLexer.cmx : cicNotationLexer.cmi
-cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \
++boxPp.cmi : \
++ mpresentation.cmi \
++ cicNotationPres.cmi \
++ box.cmi
++cicNotationLexer.cmo : \
++ cicNotationLexer.cmi
++cicNotationLexer.cmx : \
++ cicNotationLexer.cmi
+cicNotationLexer.cmi :
- cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi
- cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi
++cicNotationParser.cmo : \
++ cicNotationLexer.cmi \
++ cicNotationParser.cmi
++cicNotationParser.cmx : \
++ cicNotationLexer.cmx \
++ cicNotationParser.cmi
+cicNotationParser.cmi :
- cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \
++cicNotationPres.cmo : \
++ renderingAttrs.cmi \
++ mpresentation.cmi \
++ box.cmi \
+ cicNotationPres.cmi
- cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
++cicNotationPres.cmx : \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ box.cmx \
cicNotationPres.cmi
- cicNotationPres.cmi : mpresentation.cmi box.cmi
- content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
- cicNotationPres.cmi box.cmi content2pres.cmi
- content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
- content2pres.cmi : termContentPres.cmi cicNotationPres.cmi
- content2presMatcher.cmo : content2presMatcher.cmi
- content2presMatcher.cmx : content2presMatcher.cmi
-cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
++cicNotationPres.cmi : \
++ mpresentation.cmi \
++ box.cmi
++content2pres.cmo : \
++ termContentPres.cmi \
++ renderingAttrs.cmi \
++ mpresentation.cmi \
++ cicNotationPres.cmi \
++ box.cmi \
++ content2pres.cmi
++content2pres.cmx : \
++ termContentPres.cmx \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ cicNotationPres.cmx \
++ box.cmx \
++ content2pres.cmi
++content2pres.cmi : \
++ termContentPres.cmi \
+ cicNotationPres.cmi
-content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
- cicNotationPres.cmi box.cmi content2pres.cmi
-content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
++content2presMatcher.cmo : \
++ content2presMatcher.cmi
++content2presMatcher.cmx : \
++ content2presMatcher.cmi
+content2presMatcher.cmi :
- mpresentation.cmo : mpresentation.cmi
- mpresentation.cmx : mpresentation.cmi
++mpresentation.cmo : \
++ mpresentation.cmi
++mpresentation.cmx : \
++ mpresentation.cmi
+mpresentation.cmi :
- renderingAttrs.cmo : renderingAttrs.cmi
- renderingAttrs.cmx : renderingAttrs.cmi
++renderingAttrs.cmo : \
++ renderingAttrs.cmi
++renderingAttrs.cmx : \
++ renderingAttrs.cmi
+renderingAttrs.cmi :
- termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \
- cicNotationParser.cmi termContentPres.cmi
- termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
- termContentPres.cmi : cicNotationParser.cmi
++termContentPres.cmo : \
++ renderingAttrs.cmi \
++ content2presMatcher.cmi \
++ cicNotationParser.cmi \
++ termContentPres.cmi
++termContentPres.cmx : \
++ renderingAttrs.cmx \
++ content2presMatcher.cmx \
++ cicNotationParser.cmx \
++ termContentPres.cmi
++termContentPres.cmi : \
++ cicNotationParser.cmi
- box.cmx : renderingAttrs.cmx box.cmi
-renderingAttrs.cmi :
-cicNotationLexer.cmi :
-cicNotationParser.cmi :
-mpresentation.cmi :
++box.cmx : \
++ renderingAttrs.cmx \
++ box.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
-termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
-boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
- boxPp.cmi
--boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
++boxPp.cmx : \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ cicNotationPres.cmx \
++ box.cmx \
boxPp.cmi
- boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi
- cicNotationLexer.cmx : cicNotationLexer.cmi
-cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \
++boxPp.cmi : \
++ mpresentation.cmi \
++ cicNotationPres.cmi \
++ box.cmi
++cicNotationLexer.cmx : \
++ cicNotationLexer.cmi
+cicNotationLexer.cmi :
- cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi
++cicNotationParser.cmx : \
++ cicNotationLexer.cmx \
++ cicNotationParser.cmi
+cicNotationParser.cmi :
- cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
++cicNotationPres.cmx : \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ box.cmx \
cicNotationPres.cmi
- cicNotationPres.cmi : mpresentation.cmi box.cmi
- content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
- content2pres.cmi : termContentPres.cmi cicNotationPres.cmi
- content2presMatcher.cmx : content2presMatcher.cmi
-cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
++cicNotationPres.cmi : \
++ mpresentation.cmi \
++ box.cmi
++content2pres.cmx : \
++ termContentPres.cmx \
++ renderingAttrs.cmx \
++ mpresentation.cmx \
++ cicNotationPres.cmx \
++ box.cmx \
++ content2pres.cmi
++content2pres.cmi : \
++ termContentPres.cmi \
+ cicNotationPres.cmi
-content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
- cicNotationPres.cmi box.cmi content2pres.cmi
-content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
++content2presMatcher.cmx : \
++ content2presMatcher.cmi
+content2presMatcher.cmi :
- mpresentation.cmx : mpresentation.cmi
++mpresentation.cmx : \
++ mpresentation.cmi
+mpresentation.cmi :
- renderingAttrs.cmx : renderingAttrs.cmi
++renderingAttrs.cmx : \
++ renderingAttrs.cmi
+renderingAttrs.cmi :
- termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
- termContentPres.cmi : cicNotationParser.cmi
++termContentPres.cmx : \
++ renderingAttrs.cmx \
++ content2presMatcher.cmx \
++ cicNotationParser.cmx \
++ termContentPres.cmi
++termContentPres.cmi : \
++ cicNotationParser.cmi
- disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi
- disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi
- disambiguate.cmi : disambiguateTypes.cmi
- disambiguateTypes.cmo : disambiguateTypes.cmi
- disambiguateTypes.cmx : disambiguateTypes.cmi
++disambiguate.cmo : \
++ disambiguateTypes.cmi \
++ disambiguate.cmi
++disambiguate.cmx : \
++ disambiguateTypes.cmx \
++ disambiguate.cmi
++disambiguate.cmi : \
++ disambiguateTypes.cmi
++disambiguateTypes.cmo : \
++ disambiguateTypes.cmi
++disambiguateTypes.cmx : \
++ disambiguateTypes.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.cmo : \
++ disambiguateTypes.cmi \
++ disambiguate.cmi \
multiPassDisambiguator.cmi
--multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \
++multiPassDisambiguator.cmx : \
++ disambiguateTypes.cmx \
++ disambiguate.cmx \
multiPassDisambiguator.cmi
- multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi
++multiPassDisambiguator.cmi : \
++ disambiguateTypes.cmi \
++ disambiguate.cmi
- disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi
- disambiguate.cmi : disambiguateTypes.cmi
- disambiguateTypes.cmx : disambiguateTypes.cmi
++disambiguate.cmx : \
++ disambiguateTypes.cmx \
++ disambiguate.cmi
++disambiguate.cmi : \
++ disambiguateTypes.cmi
++disambiguateTypes.cmx : \
++ disambiguateTypes.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.cmx : disambiguateTypes.cmx disambiguate.cmx \
++multiPassDisambiguator.cmx : \
++ disambiguateTypes.cmx \
++ disambiguate.cmx \
multiPassDisambiguator.cmi
- multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi
++multiPassDisambiguator.cmi : \
++ disambiguateTypes.cmi \
++ disambiguate.cmi
- componentsConf.cmo : componentsConf.cmi
- componentsConf.cmx : componentsConf.cmi
++componentsConf.cmo : \
++ componentsConf.cmi
++componentsConf.cmx : \
++ componentsConf.cmi
componentsConf.cmi :
- discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi
- discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi
++discrimination_tree.cmo : \
++ trie.cmi \
++ hExtlib.cmi \
++ discrimination_tree.cmi
++discrimination_tree.cmx : \
++ trie.cmx \
++ hExtlib.cmx \
++ discrimination_tree.cmi
+discrimination_tree.cmi :
- graphvizPp.cmo : graphvizPp.cmi
- graphvizPp.cmx : graphvizPp.cmi
++graphvizPp.cmo : \
++ graphvizPp.cmi
++graphvizPp.cmx : \
++ graphvizPp.cmi
+graphvizPp.cmi :
- hExtlib.cmo : hExtlib.cmi
- hExtlib.cmx : hExtlib.cmi
++hExtlib.cmo : \
++ hExtlib.cmi
++hExtlib.cmx : \
++ hExtlib.cmi
hExtlib.cmi :
- hLog.cmo : hLog.cmi
- hLog.cmx : hLog.cmi
++hLog.cmo : \
++ hLog.cmi
++hLog.cmx : \
++ hLog.cmi
+hLog.cmi :
- hMarshal.cmo : hExtlib.cmi hMarshal.cmi
- hMarshal.cmx : hExtlib.cmx hMarshal.cmi
++hMarshal.cmo : \
++ hExtlib.cmi \
++ hMarshal.cmi
++hMarshal.cmx : \
++ hExtlib.cmx \
++ hMarshal.cmi
hMarshal.cmi :
- hTopoSort.cmo : hTopoSort.cmi
- hTopoSort.cmx : hTopoSort.cmi
++hTopoSort.cmo : \
++ hTopoSort.cmi
++hTopoSort.cmx : \
++ hTopoSort.cmi
+hTopoSort.cmi :
- patternMatcher.cmo : patternMatcher.cmi
- patternMatcher.cmx : patternMatcher.cmi
++patternMatcher.cmo : \
++ patternMatcher.cmi
++patternMatcher.cmx : \
++ patternMatcher.cmi
patternMatcher.cmi :
- trie.cmo : trie.cmi
- trie.cmx : trie.cmi
-hLog.cmi :
++trie.cmo : \
++ trie.cmi
++trie.cmx : \
++ trie.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.cmx : componentsConf.cmi
++componentsConf.cmx : \
++ componentsConf.cmi
componentsConf.cmi :
- discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi
++discrimination_tree.cmx : \
++ trie.cmx \
++ hExtlib.cmx \
++ discrimination_tree.cmi
+discrimination_tree.cmi :
- graphvizPp.cmx : graphvizPp.cmi
++graphvizPp.cmx : \
++ graphvizPp.cmi
+graphvizPp.cmi :
- hExtlib.cmx : hExtlib.cmi
++hExtlib.cmx : \
++ hExtlib.cmi
hExtlib.cmi :
- hLog.cmx : hLog.cmi
++hLog.cmx : \
++ hLog.cmi
+hLog.cmi :
- hMarshal.cmx : hExtlib.cmx hMarshal.cmi
++hMarshal.cmx : \
++ hExtlib.cmx \
++ hMarshal.cmi
hMarshal.cmi :
- hTopoSort.cmx : hTopoSort.cmi
++hTopoSort.cmx : \
++ hTopoSort.cmi
+hTopoSort.cmi :
- patternMatcher.cmx : patternMatcher.cmi
++patternMatcher.cmx : \
++ patternMatcher.cmi
patternMatcher.cmi :
- trie.cmx : trie.cmi
-hLog.cmi :
++trie.cmx : \
++ trie.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.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_wget.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.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.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_types.cmo
- 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_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
- http_getter_common.cmi : http_getter_types.cmo
- http_getter_const.cmo : http_getter_const.cmi
- http_getter_const.cmx : http_getter_const.cmi
++http_getter.cmi : \
++ http_getter_types.cmo
++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_common.cmx : \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_logger.cmx \
++ http_getter_env.cmx \
++ http_getter_common.cmi
++http_getter_common.cmi : \
++ http_getter_types.cmo
++http_getter_const.cmo : \
++ http_getter_const.cmi
++http_getter_const.cmx : \
++ http_getter_const.cmi
+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_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
- http_getter_env.cmi : http_getter_types.cmo
- http_getter_logger.cmo : http_getter_logger.cmi
- http_getter_logger.cmx : http_getter_logger.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_env.cmx : \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_logger.cmx \
++ http_getter_const.cmx \
++ http_getter_env.cmi
++http_getter_env.cmi : \
++ http_getter_types.cmo
++http_getter_logger.cmo : \
++ http_getter_logger.cmi
++http_getter_logger.cmx : \
++ http_getter_logger.cmi
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_misc.cmo : \
++ http_getter_logger.cmi \
++ http_getter_misc.cmi
++http_getter_misc.cmx : \
++ http_getter_logger.cmx \
++ http_getter_misc.cmi
http_getter_misc.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_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
- http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
-http_getter_const.cmi :
-http_getter_env.cmi : http_getter_types.cmo
++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_storage.cmx : \
++ http_getter_wget.cmx \
++ http_getter_types.cmx \
++ http_getter_misc.cmx \
++ http_getter_env.cmx \
++ http_getter_storage.cmi
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_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
- 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_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
- 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_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
- 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.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_wget.cmo : \
++ http_getter_types.cmo \
++ http_getter_wget.cmi
++http_getter_wget.cmx : \
++ http_getter_types.cmx \
++ http_getter_wget.cmi
+http_getter_wget.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_wget.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_types.cmx
- 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_common.cmi : http_getter_types.cmx
- http_getter_const.cmx : http_getter_const.cmi
++http_getter.cmi : \
++ http_getter_types.cmx
++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_common.cmi : \
++ http_getter_types.cmx
++http_getter_const.cmx : \
++ http_getter_const.cmi
+http_getter_const.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_env.cmi : http_getter_types.cmx
- http_getter_logger.cmx : http_getter_logger.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_env.cmi : \
++ http_getter_types.cmx
++http_getter_logger.cmx : \
++ http_getter_logger.cmi
http_getter_logger.cmi :
- http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi
++http_getter_misc.cmx : \
++ http_getter_logger.cmx \
++ http_getter_misc.cmi
http_getter_misc.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_const.cmi :
-http_getter_env.cmi : http_getter_types.cmx
++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_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_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
- 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_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
- 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_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
- 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.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_wget.cmx : \
++ http_getter_types.cmx \
++ http_getter_wget.cmi
+http_getter_wget.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
++grafiteAstPp.cmo : \
++ grafiteAst.cmo \
++ grafiteAstPp.cmi
++grafiteAstPp.cmx : \
++ grafiteAst.cmx \
++ grafiteAstPp.cmi
++grafiteAstPp.cmi : \
++ grafiteAst.cmo
-grafiteAstPp.cmi : grafiteAst.cmx
-grafiteAst.cmo :
grafiteAst.cmx :
-grafiteAstPp.cmo : grafiteAst.cmx grafiteAstPp.cmi
--grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi
- grafiteAstPp.cmi : grafiteAst.cmx
++grafiteAstPp.cmx : \
++ grafiteAst.cmx \
++ grafiteAstPp.cmi
++grafiteAstPp.cmi : \
++ grafiteAst.cmx
| NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
- | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^
- | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^
++ | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^
" with " ^ NotationPp.pp_term status wwhat
| NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t
| NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *)
| NClear (_,l) -> "nclear " ^ String.concat " " l
- | NDestruct (_,_dom,_skip) -> "ndestruct ..."
- | NDestruct (_,dom,skip) -> "ndestruct ..."
- | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term status what ^
++ | NDestruct (_,_dom,_skip) -> "ndestruct ..."
+ | NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
| NSkip _ -> "skip"
| NTry (_,tac) -> "ntry " ^ pp_ntactic status ~map_unicode_to_tex tac
| NAssumption _ -> "nassumption"
- | NBlock (_,l) ->
+ | NBlock (_,l) ->
"(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")"
| NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t
+ | Assume (_, ident, term) -> "assume " ^ ident ^ ":(" ^ (NotationPp.pp_term status term) ^ ")"
+ | Suppose (_,term,ident) -> "suppose (" ^ (NotationPp.pp_term status term) ^ ") (" ^ ident ^ ") "
+ | By_just_we_proved (_, just, term1, ident) -> pp_just status just ^ " we proved (" ^
+ (NotationPp.pp_term status term1) ^ ")" ^ (match ident with
+ None -> "" | Some ident -> "(" ^ident^ ")")
+ | We_need_to_prove (_,term,ident) -> "we need to prove (" ^ (NotationPp.pp_term status term) ^ ") " ^
+ (match ident with None -> "" | Some id -> "(" ^ id ^ ")")
+ | BetaRewritingStep (_,t) -> "that is equivalent to (" ^ (NotationPp.pp_term status t) ^ ")"
+ | Bydone (_, just) -> pp_just status just ^ "done"
+ | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ": ("
+ ^ (NotationPp.pp_term status term) ^ ") such that (" ^ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ")"
+ | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ " we have (" ^
+ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ") " ^ "and (" ^ (NotationPp.pp_term status
+ term2)
+ ^ ") (" ^ ident2 ^ ")"
+ | Thesisbecomes (_, t) -> "the thesis becomes (" ^ (NotationPp.pp_term status t) ^ ")"
+ | RewritingStep (_, rhs, just, cont) ->
+ "= (" ^
+ (NotationPp.pp_term status rhs) ^ ")" ^
+ (match just with
+ | `Auto params -> let s = pp_auto_params params status in
+ if s <> "" then " by " ^ s
+ else ""
+ | `Term t -> " exact (" ^ (NotationPp.pp_term status t) ^ ")"
+ | `Proof -> " proof"
+ | `SolveWith t -> " using (" ^ (NotationPp.pp_term status t) ^ ")"
+ )
+ ^ (if cont then " done" else "")
+ | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ " (" ^ (NotationPp.pp_term status t1) ^ ")"
+ | Conclude (_,t1) -> "conclude (" ^ (NotationPp.pp_term status t1) ^ ")"
+ | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on (" ^ NotationPp.pp_term
+ status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")"
+ | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on (" ^
+ NotationPp.pp_term status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")"
+ | Byinduction (_, term, ident) -> "by induction hypothesis we know (" ^ NotationPp.pp_term status
+ term ^ ") (" ^ ident ^ ")"
+ | Case (_, id, args) ->
+ "case " ^ id ^
+ String.concat " "
+ (List.map (function (id,term) -> "(" ^ id ^ ": (" ^ NotationPp.pp_term status term ^ "))")
+ args)
++ | PrintStack _ -> "print_stack"
;;
let pp_nmacro status = function
-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.cmo : \
++ nCicCoercDeclaration.cmi \
++ grafiteTypes.cmi \
grafiteEngine.cmi
--grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \
++grafiteEngine.cmx : \
++ nCicCoercDeclaration.cmx \
++ grafiteTypes.cmx \
grafiteEngine.cmi
- grafiteEngine.cmi : grafiteTypes.cmi
- grafiteTypes.cmo : grafiteTypes.cmi
- grafiteTypes.cmx : grafiteTypes.cmi
++grafiteEngine.cmi : \
++ grafiteTypes.cmi
++grafiteTypes.cmo : \
++ grafiteTypes.cmi
++grafiteTypes.cmx : \
++ grafiteTypes.cmi
+grafiteTypes.cmi :
- nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi
- nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi
- nCicCoercDeclaration.cmi : grafiteTypes.cmi
++nCicCoercDeclaration.cmo : \
++ grafiteTypes.cmi \
++ nCicCoercDeclaration.cmi
++nCicCoercDeclaration.cmx : \
++ grafiteTypes.cmx \
++ nCicCoercDeclaration.cmi
++nCicCoercDeclaration.cmi : \
++ grafiteTypes.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.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \
++grafiteEngine.cmx : \
++ nCicCoercDeclaration.cmx \
++ grafiteTypes.cmx \
grafiteEngine.cmi
- grafiteEngine.cmi : grafiteTypes.cmi
- grafiteTypes.cmx : grafiteTypes.cmi
++grafiteEngine.cmi : \
++ grafiteTypes.cmi
++grafiteTypes.cmx : \
++ grafiteTypes.cmi
+grafiteTypes.cmi :
- nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi
- nCicCoercDeclaration.cmi : grafiteTypes.cmi
++nCicCoercDeclaration.cmx : \
++ grafiteTypes.cmx \
++ nCicCoercDeclaration.cmi
++nCicCoercDeclaration.cmi : \
++ grafiteTypes.cmi
NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
|GrafiteAst.NRepeat (_,tac) ->
NTactics.repeat_tac (f f (text, prefix_len, tac))
- `Term t -> just_to_tacstatus_just just text prefix_len
- | `Auto params -> just_to_tacstatus_just just text prefix_len
+ |GrafiteAst.Assume (_,id,t) -> Declarative.assume id (text,prefix_len,t)
+ |GrafiteAst.Suppose (_,t,id) -> Declarative.suppose (text,prefix_len,t) id
+ |GrafiteAst.By_just_we_proved (_,j,t1,s) -> Declarative.by_just_we_proved
+ (just_to_tacstatus_just j text prefix_len) (text,prefix_len,t1) s
+ |GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove (text,prefix_len,t) id
+ |GrafiteAst.BetaRewritingStep (_, t) -> Declarative.beta_rewriting_step (text,prefix_len,t)
+ | GrafiteAst.Bydone (_, j) -> Declarative.bydone (just_to_tacstatus_just j text prefix_len)
+ | GrafiteAst.ExistsElim (_, just, id1, t1, t2, id2) ->
+ Declarative.existselim (just_to_tacstatus_just just text prefix_len) id1 (text,prefix_len,t1)
+ (text,prefix_len,t2) id2
+ | GrafiteAst.AndElim(_,just,t1,id1,t2,id2) -> Declarative.andelim (just_to_tacstatus_just just
+ text prefix_len) (text,prefix_len,t1) id1 (text,prefix_len,t2) id2
+ | GrafiteAst.Thesisbecomes (_, t1) -> Declarative.thesisbecomes (text,prefix_len,t1)
+ | GrafiteAst.RewritingStep (_,rhs,just,cont) ->
+ Declarative.rewritingstep (text,prefix_len,rhs)
+ (match just with
++ `Term _
++ | `Auto _ -> just_to_tacstatus_just just text prefix_len
+ |`Proof -> `Proof
+ |`SolveWith t -> `SolveWith (text,prefix_len,t)
+ )
+ cont
+ | GrafiteAst.Obtain (_,id,t1) ->
+ Declarative.obtain id (text,prefix_len,t1)
+ | GrafiteAst.Conclude (_,t1) ->
+ Declarative.conclude (text,prefix_len,t1)
+ | GrafiteAst.We_proceed_by_cases_on (_, t, t1) ->
+ Declarative.we_proceed_by_cases_on (text,prefix_len,t) (text,prefix_len,t1)
+ | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
+ Declarative.we_proceed_by_induction_on (text,prefix_len,t) (text,prefix_len,t1)
+ | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction (text,prefix_len,t) id
+ | GrafiteAst.Case (_,id,params) -> Declarative.case id params
+ | GrafiteAst.PrintStack (_) -> Declarative.print_stack
in
aux aux tac (* trick for non uniform recursion call *)
;;
- grafiteParser.cmo : grafiteParser.cmi
- grafiteParser.cmx : grafiteParser.cmi
++grafiteParser.cmo : \
++ grafiteParser.cmi
++grafiteParser.cmx : \
++ grafiteParser.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
- print_grammar.cmi : grafiteParser.cmi
++print_grammar.cmo : \
++ print_grammar.cmi
++print_grammar.cmx : \
++ print_grammar.cmi
++print_grammar.cmi : \
++ grafiteParser.cmi
- grafiteParser.cmx : grafiteParser.cmi
++grafiteParser.cmx : \
++ grafiteParser.cmi
grafiteParser.cmi :
- print_grammar.cmx : print_grammar.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
++print_grammar.cmx : \
++ print_grammar.cmi
++print_grammar.cmi : \
++ grafiteParser.cmi
- librarian.cmo : librarian.cmi
- librarian.cmx : librarian.cmi
++librarian.cmo : \
++ librarian.cmi
++librarian.cmx : \
++ librarian.cmi
librarian.cmi :
- libraryClean.cmo : libraryClean.cmi
- libraryClean.cmx : libraryClean.cmi
-libraryMisc.cmi :
++libraryClean.cmo : \
++ libraryClean.cmi
++libraryClean.cmx : \
++ libraryClean.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
++libraryMisc.cmo : \
++ libraryMisc.cmi
++libraryMisc.cmx : \
++ libraryMisc.cmi
+libraryMisc.cmi :
- librarian.cmx : librarian.cmi
++librarian.cmx : \
++ librarian.cmi
librarian.cmi :
- libraryClean.cmx : libraryClean.cmi
-libraryMisc.cmi :
++libraryClean.cmx : \
++ libraryClean.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
++libraryMisc.cmx : \
++ libraryMisc.cmi
+libraryMisc.cmi :
- helmLogger.cmo : helmLogger.cmi
- helmLogger.cmx : helmLogger.cmi
++helmLogger.cmo : \
++ helmLogger.cmi
++helmLogger.cmx : \
++ helmLogger.cmi
helmLogger.cmi :
-helmLogger.cmo : helmLogger.cmi
-helmLogger.cmx : helmLogger.cmi
- helmLogger.cmx : helmLogger.cmi
++helmLogger.cmx : \
++ helmLogger.cmi
helmLogger.cmi :
-helmLogger.cmo : helmLogger.cmi
-helmLogger.cmx : helmLogger.cmi
- interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi
- interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
-ncic2astMatcher.cmi :
++interpretations.cmo : \
++ ncic2astMatcher.cmi \
++ interpretations.cmi
++interpretations.cmx : \
++ ncic2astMatcher.cmx \
++ interpretations.cmi
interpretations.cmi :
--ncic2astMatcher.cmo : ncic2astMatcher.cmi
--ncic2astMatcher.cmx : ncic2astMatcher.cmi
-interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi
-interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
++ncic2astMatcher.cmo : \
++ ncic2astMatcher.cmi
++ncic2astMatcher.cmx : \
++ ncic2astMatcher.cmi
+ncic2astMatcher.cmi :
- interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
-ncic2astMatcher.cmi :
++interpretations.cmx : \
++ ncic2astMatcher.cmx \
++ interpretations.cmi
interpretations.cmi :
-ncic2astMatcher.cmo : ncic2astMatcher.cmi
--ncic2astMatcher.cmx : ncic2astMatcher.cmi
-interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi
-interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
++ncic2astMatcher.cmx : \
++ ncic2astMatcher.cmi
+ncic2astMatcher.cmi :
- disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi
- disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
-nnumber_notation.cmi :
++disambiguateChoices.cmo : \
++ nnumber_notation.cmi \
++ disambiguateChoices.cmi
++disambiguateChoices.cmx : \
++ nnumber_notation.cmx \
++ disambiguateChoices.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.cmo : \
++ nCicDisambiguate.cmi \
++ disambiguateChoices.cmi \
grafiteDisambiguate.cmi
--grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \
++grafiteDisambiguate.cmx : \
++ nCicDisambiguate.cmx \
++ disambiguateChoices.cmx \
grafiteDisambiguate.cmi
- nCicDisambiguate.cmo : nCicDisambiguate.cmi
- nCicDisambiguate.cmx : nCicDisambiguate.cmi
+grafiteDisambiguate.cmi :
- nnumber_notation.cmo : nnumber_notation.cmi
- nnumber_notation.cmx : nnumber_notation.cmi
++nCicDisambiguate.cmo : \
++ nCicDisambiguate.cmi
++nCicDisambiguate.cmx : \
++ nCicDisambiguate.cmi
+nCicDisambiguate.cmi :
++nnumber_notation.cmo : \
++ nnumber_notation.cmi
++nnumber_notation.cmx : \
++ nnumber_notation.cmi
+nnumber_notation.cmi :
- disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
-nnumber_notation.cmi :
++disambiguateChoices.cmx : \
++ nnumber_notation.cmx \
++ disambiguateChoices.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.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \
++grafiteDisambiguate.cmx : \
++ nCicDisambiguate.cmx \
++ disambiguateChoices.cmx \
grafiteDisambiguate.cmi
- nCicDisambiguate.cmx : nCicDisambiguate.cmi
+grafiteDisambiguate.cmi :
- nnumber_notation.cmx : nnumber_notation.cmi
++nCicDisambiguate.cmx : \
++ nCicDisambiguate.cmi
+nCicDisambiguate.cmi :
++nnumber_notation.cmx : \
++ nnumber_notation.cmi
+nnumber_notation.cmi :
- common.cmo : ocamlExtractionTable.cmi mlutil.cmi coq.cmi common.cmi
- common.cmx : ocamlExtractionTable.cmx mlutil.cmx coq.cmx common.cmi
- common.cmi : ocamlExtractionTable.cmi coq.cmi
-nCicExtraction.cmi :
-coq.cmi :
-ocamlExtractionTable.cmi : miniml.cmo coq.cmi
-mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
-common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi
-extraction.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
-ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
-ocamlExtraction.cmi : ocamlExtractionTable.cmi
-miniml.cmo : coq.cmi
-miniml.cmx : coq.cmx
-nCicExtraction.cmo : nCicExtraction.cmi
-nCicExtraction.cmx : nCicExtraction.cmi
--coq.cmo : coq.cmi
--coq.cmx : coq.cmi
-ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi
-ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
-mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi
-mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
-common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
++common.cmo : \
++ ocamlExtractionTable.cmi \
++ mlutil.cmi \
++ coq.cmi \
+ common.cmi
-common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
++common.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ coq.cmx \
+ common.cmi
-extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
- common.cmi extraction.cmi
-extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx extraction.cmi
-ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
- common.cmi ocaml.cmi
-ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx ocaml.cmi
-ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \
- coq.cmi ocamlExtraction.cmi
-ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
- coq.cmx ocamlExtraction.cmi
++common.cmi : \
++ ocamlExtractionTable.cmi \
++ coq.cmi
++coq.cmo : \
++ coq.cmi
++coq.cmx : \
++ coq.cmi
+coq.cmi :
- extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
- common.cmi extraction.cmi
- extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx extraction.cmi
- extraction.cmi : ocamlExtractionTable.cmi miniml.cmo
- miniml.cmo : coq.cmi
- miniml.cmx : coq.cmx
- mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi
- mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
- mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
- nCicExtraction.cmo : nCicExtraction.cmi
- nCicExtraction.cmx : nCicExtraction.cmi
++extraction.cmo : \
++ ocamlExtractionTable.cmi \
++ mlutil.cmi \
++ miniml.cmo \
++ coq.cmi \
++ common.cmi \
++ extraction.cmi
++extraction.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ miniml.cmx \
++ coq.cmx \
++ common.cmx \
++ extraction.cmi
++extraction.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmo
++miniml.cmo : \
++ coq.cmi
++miniml.cmx : \
++ coq.cmx
++mlutil.cmo : \
++ ocamlExtractionTable.cmi \
++ miniml.cmo \
++ coq.cmi \
++ mlutil.cmi
++mlutil.cmx : \
++ ocamlExtractionTable.cmx \
++ miniml.cmx \
++ coq.cmx \
++ mlutil.cmi
++mlutil.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmo \
++ coq.cmi
++nCicExtraction.cmo : \
++ nCicExtraction.cmi
++nCicExtraction.cmx : \
++ nCicExtraction.cmi
+nCicExtraction.cmi :
- ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
- common.cmi ocaml.cmi
- ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx ocaml.cmi
- ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
- ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \
- coq.cmi ocamlExtraction.cmi
- ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
- coq.cmx ocamlExtraction.cmi
- ocamlExtraction.cmi : ocamlExtractionTable.cmi
- ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi
- ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
- ocamlExtractionTable.cmi : miniml.cmo coq.cmi
++ocaml.cmo : \
++ ocamlExtractionTable.cmi \
++ mlutil.cmi \
++ miniml.cmo \
++ coq.cmi \
++ common.cmi \
++ ocaml.cmi
++ocaml.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ miniml.cmx \
++ coq.cmx \
++ common.cmx \
++ ocaml.cmi
++ocaml.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmo \
++ coq.cmi
++ocamlExtraction.cmo : \
++ ocamlExtractionTable.cmi \
++ ocaml.cmi \
++ extraction.cmi \
++ coq.cmi \
++ ocamlExtraction.cmi
++ocamlExtraction.cmx : \
++ ocamlExtractionTable.cmx \
++ ocaml.cmx \
++ extraction.cmx \
++ coq.cmx \
++ ocamlExtraction.cmi
++ocamlExtraction.cmi : \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmo : \
++ miniml.cmo \
++ coq.cmi \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmx : \
++ miniml.cmx \
++ coq.cmx \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmi : \
++ miniml.cmo \
++ coq.cmi
- common.cmx : ocamlExtractionTable.cmx mlutil.cmx coq.cmx common.cmi
- common.cmi : ocamlExtractionTable.cmi coq.cmi
-nCicExtraction.cmi :
-coq.cmi :
-ocamlExtractionTable.cmi : miniml.cmx coq.cmi
-mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
-common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi
-extraction.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
-ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
-ocamlExtraction.cmi : ocamlExtractionTable.cmi
-miniml.cmo : coq.cmi
-miniml.cmx : coq.cmx
-nCicExtraction.cmo : nCicExtraction.cmi
-nCicExtraction.cmx : nCicExtraction.cmi
-coq.cmo : coq.cmi
--coq.cmx : coq.cmi
-ocamlExtractionTable.cmo : miniml.cmx coq.cmi ocamlExtractionTable.cmi
-ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
-mlutil.cmo : ocamlExtractionTable.cmi miniml.cmx coq.cmi mlutil.cmi
-mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
-common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \
- common.cmi
-common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
++common.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ coq.cmx \
+ common.cmi
-extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \
- common.cmi extraction.cmi
-extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx extraction.cmi
-ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \
- common.cmi ocaml.cmi
-ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx ocaml.cmi
-ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \
- coq.cmi ocamlExtraction.cmi
-ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
- coq.cmx ocamlExtraction.cmi
++common.cmi : \
++ ocamlExtractionTable.cmi \
++ coq.cmi
++coq.cmx : \
++ coq.cmi
+coq.cmi :
- extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx extraction.cmi
- extraction.cmi : ocamlExtractionTable.cmi miniml.cmx
- miniml.cmx : coq.cmx
- mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
- mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
- nCicExtraction.cmx : nCicExtraction.cmi
++extraction.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ miniml.cmx \
++ coq.cmx \
++ common.cmx \
++ extraction.cmi
++extraction.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmx
++miniml.cmx : \
++ coq.cmx
++mlutil.cmx : \
++ ocamlExtractionTable.cmx \
++ miniml.cmx \
++ coq.cmx \
++ mlutil.cmi
++mlutil.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmx \
++ coq.cmi
++nCicExtraction.cmx : \
++ nCicExtraction.cmi
+nCicExtraction.cmi :
- ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
- common.cmx ocaml.cmi
- ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
- ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
- coq.cmx ocamlExtraction.cmi
- ocamlExtraction.cmi : ocamlExtractionTable.cmi
- ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
- ocamlExtractionTable.cmi : miniml.cmx coq.cmi
++ocaml.cmx : \
++ ocamlExtractionTable.cmx \
++ mlutil.cmx \
++ miniml.cmx \
++ coq.cmx \
++ common.cmx \
++ ocaml.cmi
++ocaml.cmi : \
++ ocamlExtractionTable.cmi \
++ miniml.cmx \
++ coq.cmi
++ocamlExtraction.cmx : \
++ ocamlExtractionTable.cmx \
++ ocaml.cmx \
++ extraction.cmx \
++ coq.cmx \
++ ocamlExtraction.cmi
++ocamlExtraction.cmi : \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmx : \
++ miniml.cmx \
++ coq.cmx \
++ ocamlExtractionTable.cmi
++ocamlExtractionTable.cmi : \
++ miniml.cmx \
++ coq.cmi
let n = List.length i in
let cand = lift n cand in
let cand = pop n (non_stricts add cand t) in
- List.merge (compare) cand c) [] v
- List.merge (fun c1 c2 -> c1 - c2) cand c) [] v
++ List.merge (-) cand c) [] v
(* [merge] may duplicates some indices, but I don't mind. *)
| MLmagic t ->
non_stricts add cand t
- nCic.cmo : nUri.cmi nReference.cmi
- nCic.cmx : nUri.cmx nReference.cmx
- nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi
- nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
-nUri.cmi :
-nReference.cmi : nUri.cmi
-nCicUtils.cmi : nCic.cmo
-nCicSubstitution.cmi : nCic.cmo
--nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmo
- nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
- nCicEnvironment.cmi nCic.cmo nCicPp.cmi
- nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
- nCicPp.cmi : nReference.cmi nCic.cmo
- nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmo nCicReduction.cmi
- nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
--nCicReduction.cmi : nCic.cmo
- nCicSubstitution.cmo : nCicUtils.cmi nCic.cmo nCicSubstitution.cmi
- nCicSubstitution.cmx : nCicUtils.cmx nCic.cmx nCicSubstitution.cmi
- nCicSubstitution.cmi : nCic.cmo
- nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \
- nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.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 \
++nCic.cmo : \
++ nUri.cmi \
++ nReference.cmi
++nCic.cmx : \
++ nUri.cmx \
++ nReference.cmx
++nCicEnvironment.cmo : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmo \
++ nCicEnvironment.cmi
++nCicEnvironment.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCic.cmx \
++ nCicEnvironment.cmi
++nCicEnvironment.cmi : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmo
++nCicPp.cmo : \
++ nUri.cmi \
++ nReference.cmi \
++ nCicSubstitution.cmi \
++ nCicReduction.cmi \
++ nCicEnvironment.cmi \
++ nCic.cmo \
++ nCicPp.cmi
++nCicPp.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicPp.cmi
++nCicPp.cmi : \
++ nReference.cmi \
++ nCic.cmo
++nCicReduction.cmo : \
++ nReference.cmi \
++ nCicUtils.cmi \
++ nCicSubstitution.cmi \
++ nCicEnvironment.cmi \
++ nCic.cmo \
++ nCicReduction.cmi
++nCicReduction.cmx : \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicReduction.cmi
++nCicReduction.cmi : \
++ nCic.cmo
++nCicSubstitution.cmo : \
++ nCicUtils.cmi \
++ nCic.cmo \
+ nCicSubstitution.cmi
-nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \
++nCicSubstitution.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
-nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmo nCicReduction.cmi
-nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
-nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \
- nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \
++nCicSubstitution.cmi : \
++ nCic.cmo
++nCicTypeChecker.cmo : \
++ nUri.cmi \
++ nReference.cmi \
++ nCicUtils.cmi \
++ nCicSubstitution.cmi \
++ nCicReduction.cmi \
++ nCicEnvironment.cmi \
++ nCic.cmo \
nCicTypeChecker.cmi
--nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \
-- nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
++nCicTypeChecker.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
nCicTypeChecker.cmi
- nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmo
--nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.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
- nCicUntrusted.cmi : nCic.cmo
- nCicUtils.cmo : nCic.cmo nCicUtils.cmi
- nCicUtils.cmx : nCic.cmx nCicUtils.cmi
- nCicUtils.cmi : nCic.cmo
- nReference.cmo : nUri.cmi nReference.cmi
- nReference.cmx : nUri.cmx nReference.cmi
- nReference.cmi : nUri.cmi
- nUri.cmo : nUri.cmi
- nUri.cmx : nUri.cmi
-nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
- nCicEnvironment.cmi nCic.cmo nCicPp.cmi
-nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
++nCicTypeChecker.cmi : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmo
++nCicUntrusted.cmo : \
++ nReference.cmi \
++ nCicUtils.cmi \
++ nCicSubstitution.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
++nCicUntrusted.cmi : \
++ nCic.cmo
++nCicUtils.cmo : \
++ nCic.cmo \
++ nCicUtils.cmi
++nCicUtils.cmx : \
++ nCic.cmx \
++ nCicUtils.cmi
++nCicUtils.cmi : \
++ nCic.cmo
++nReference.cmo : \
++ nUri.cmi \
++ nReference.cmi
++nReference.cmx : \
++ nUri.cmx \
++ nReference.cmi
++nReference.cmi : \
++ nUri.cmi
++nUri.cmo : \
++ nUri.cmi
++nUri.cmx : \
++ nUri.cmi
+nUri.cmi :
- nCic.cmx : nUri.cmx nReference.cmx
- nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
-nUri.cmi :
-nReference.cmi : nUri.cmi
-nCicUtils.cmi : nCic.cmx
-nCicSubstitution.cmi : nCic.cmx
--nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmx
- nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
- nCicPp.cmi : nReference.cmi nCic.cmx
- nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
--nCicReduction.cmi : nCic.cmx
- nCicSubstitution.cmx : nCicUtils.cmx nCic.cmx nCicSubstitution.cmi
- nCicSubstitution.cmi : nCic.cmx
- nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \
- nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx 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.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \
++nCic.cmx : \
++ nUri.cmx \
++ nReference.cmx
++nCicEnvironment.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCic.cmx \
++ nCicEnvironment.cmi
++nCicEnvironment.cmi : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmx
++nCicPp.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicPp.cmi
++nCicPp.cmi : \
++ nReference.cmi \
++ nCic.cmx
++nCicReduction.cmx : \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicReduction.cmi
++nCicReduction.cmi : \
++ nCic.cmx
++nCicSubstitution.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
-nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmx nCicReduction.cmi
-nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
-nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \
- nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \
++nCicSubstitution.cmi : \
++ nCic.cmx
++nCicTypeChecker.cmx : \
++ nUri.cmx \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
nCicTypeChecker.cmi
- nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx
-nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \
- nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
- nCicTypeChecker.cmi
-nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.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
- nCicUntrusted.cmi : nCic.cmx
- nCicUtils.cmx : nCic.cmx nCicUtils.cmi
- nCicUtils.cmi : nCic.cmx
- nReference.cmx : nUri.cmx nReference.cmi
- nReference.cmi : nUri.cmi
- nUri.cmx : nUri.cmi
-nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
- nCicEnvironment.cmi nCic.cmx nCicPp.cmi
-nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
++nCicTypeChecker.cmi : \
++ nUri.cmi \
++ nReference.cmi \
++ nCic.cmx
++nCicUntrusted.cmx : \
++ nReference.cmx \
++ nCicUtils.cmx \
++ nCicSubstitution.cmx \
++ nCicReduction.cmx \
++ nCicEnvironment.cmx \
++ nCic.cmx \
++ nCicUntrusted.cmi
++nCicUntrusted.cmi : \
++ nCic.cmx
++nCicUtils.cmx : \
++ nCic.cmx \
++ nCicUtils.cmi
++nCicUtils.cmi : \
++ nCic.cmx
++nReference.cmx : \
++ nUri.cmx \
++ nReference.cmi
++nReference.cmi : \
++ nUri.cmi
++nUri.cmx : \
++ nUri.cmi
+nUri.cmi :
- nCicLibrary.cmo : nCicLibrary.cmi
- nCicLibrary.cmx : nCicLibrary.cmi
++nCicLibrary.cmo : \
++ nCicLibrary.cmi
++nCicLibrary.cmx : \
++ nCicLibrary.cmi
nCicLibrary.cmi :
-nCicLibrary.cmo : nCicLibrary.cmi
-nCicLibrary.cmx : nCicLibrary.cmi
- nCicLibrary.cmx : nCicLibrary.cmi
++nCicLibrary.cmx : \
++ nCicLibrary.cmi
nCicLibrary.cmi :
-nCicLibrary.cmo : nCicLibrary.cmi
-nCicLibrary.cmx : nCicLibrary.cmi
- foSubst.cmo : terms.cmi foSubst.cmi
- foSubst.cmx : terms.cmx foSubst.cmi
- foSubst.cmi : terms.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
- foUnif.cmi : terms.cmi orderings.cmi
- foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
- foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
- foUtils.cmi : terms.cmi orderings.cmi
- index.cmo : terms.cmi orderings.cmi foUtils.cmi index.cmi
- index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi
- index.cmi : terms.cmi orderings.cmi
- nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi
- nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi
- nCicBlob.cmi : terms.cmi
- nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
- nCicBlob.cmi nCicParamod.cmi
- nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
- nCicBlob.cmx nCicParamod.cmi
- nCicParamod.cmi : terms.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
- nCicProof.cmi : terms.cmi
- orderings.cmo : terms.cmi foSubst.cmi orderings.cmi
- orderings.cmx : terms.cmx foSubst.cmx orderings.cmi
- orderings.cmi : terms.cmi
- paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
- foUtils.cmi paramod.cmi
- paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
- foUtils.cmx paramod.cmi
- paramod.cmi : terms.cmi orderings.cmi
- pp.cmo : terms.cmi pp.cmi
- pp.cmx : terms.cmx pp.cmi
- pp.cmi : terms.cmi
- stats.cmo : terms.cmi stats.cmi
- stats.cmx : terms.cmx stats.cmi
- stats.cmi : terms.cmi orderings.cmi
- superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.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
- superposition.cmi : terms.cmi orderings.cmi index.cmi
- terms.cmo : terms.cmi
- terms.cmx : terms.cmi
++foSubst.cmo : \
++ terms.cmi \
++ foSubst.cmi
++foSubst.cmx : \
++ terms.cmx \
++ foSubst.cmi
++foSubst.cmi : \
++ terms.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
++foUnif.cmi : \
++ terms.cmi \
++ orderings.cmi
++foUtils.cmo : \
++ terms.cmi \
++ orderings.cmi \
++ foSubst.cmi \
++ foUtils.cmi
++foUtils.cmx : \
++ terms.cmx \
++ orderings.cmx \
++ foSubst.cmx \
++ foUtils.cmi
++foUtils.cmi : \
++ terms.cmi \
++ orderings.cmi
++index.cmo : \
++ terms.cmi \
++ orderings.cmi \
++ foUtils.cmi \
++ index.cmi
++index.cmx : \
++ terms.cmx \
++ orderings.cmx \
++ foUtils.cmx \
++ index.cmi
++index.cmi : \
++ terms.cmi \
++ orderings.cmi
++nCicBlob.cmo : \
++ terms.cmi \
++ foUtils.cmi \
++ nCicBlob.cmi
++nCicBlob.cmx : \
++ terms.cmx \
++ foUtils.cmx \
++ nCicBlob.cmi
++nCicBlob.cmi : \
++ terms.cmi
++nCicParamod.cmo : \
++ terms.cmi \
++ pp.cmi \
++ paramod.cmi \
++ orderings.cmi \
++ nCicProof.cmi \
++ nCicBlob.cmi \
++ nCicParamod.cmi
++nCicParamod.cmx : \
++ terms.cmx \
++ pp.cmx \
++ paramod.cmx \
++ orderings.cmx \
++ nCicProof.cmx \
++ nCicBlob.cmx \
++ nCicParamod.cmi
++nCicParamod.cmi : \
++ terms.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
++nCicProof.cmi : \
++ terms.cmi
++orderings.cmo : \
++ terms.cmi \
++ foSubst.cmi \
++ orderings.cmi
++orderings.cmx : \
++ terms.cmx \
++ foSubst.cmx \
++ orderings.cmi
++orderings.cmi : \
++ terms.cmi
++paramod.cmo : \
++ terms.cmi \
++ superposition.cmi \
++ pp.cmi \
++ orderings.cmi \
++ index.cmi \
++ foUtils.cmi \
++ paramod.cmi
++paramod.cmx : \
++ terms.cmx \
++ superposition.cmx \
++ pp.cmx \
++ orderings.cmx \
++ index.cmx \
++ foUtils.cmx \
++ paramod.cmi
++paramod.cmi : \
++ terms.cmi \
++ orderings.cmi
++pp.cmo : \
++ terms.cmi \
++ pp.cmi
++pp.cmx : \
++ terms.cmx \
++ pp.cmi
++pp.cmi : \
++ terms.cmi
++stats.cmo : \
++ terms.cmi \
++ stats.cmi
++stats.cmx : \
++ terms.cmx \
++ stats.cmi
++stats.cmi : \
++ terms.cmi \
++ orderings.cmi
++superposition.cmo : \
++ terms.cmi \
++ pp.cmi \
++ orderings.cmi \
++ index.cmi \
++ foUtils.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
++superposition.cmi : \
++ terms.cmi \
++ orderings.cmi \
++ index.cmi
++terms.cmo : \
++ terms.cmi
++terms.cmx : \
++ terms.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.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
-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
-paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.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
-nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
- nCicBlob.cmi nCicParamod.cmi
-nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
- nCicBlob.cmx nCicParamod.cmi
- foSubst.cmx : terms.cmx foSubst.cmi
- foSubst.cmi : terms.cmi
- foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
- foUnif.cmi : terms.cmi orderings.cmi
- foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
- foUtils.cmi : terms.cmi orderings.cmi
- index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi
- index.cmi : terms.cmi orderings.cmi
- nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi
- nCicBlob.cmi : terms.cmi
- nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
- nCicBlob.cmx nCicParamod.cmi
- nCicParamod.cmi : terms.cmi
- nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
- nCicProof.cmi : terms.cmi
- orderings.cmx : terms.cmx foSubst.cmx orderings.cmi
- orderings.cmi : terms.cmi
- paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
- foUtils.cmx paramod.cmi
- paramod.cmi : terms.cmi orderings.cmi
- pp.cmx : terms.cmx pp.cmi
- pp.cmi : terms.cmi
- stats.cmx : terms.cmx stats.cmi
- stats.cmi : terms.cmi orderings.cmi
- superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
- foUnif.cmx foSubst.cmx superposition.cmi
- superposition.cmi : terms.cmi orderings.cmi index.cmi
- terms.cmx : terms.cmi
++foSubst.cmx : \
++ terms.cmx \
++ foSubst.cmi
++foSubst.cmi : \
++ terms.cmi
++foUnif.cmx : \
++ terms.cmx \
++ orderings.cmx \
++ foUtils.cmx \
++ foSubst.cmx \
++ foUnif.cmi
++foUnif.cmi : \
++ terms.cmi \
++ orderings.cmi
++foUtils.cmx : \
++ terms.cmx \
++ orderings.cmx \
++ foSubst.cmx \
++ foUtils.cmi
++foUtils.cmi : \
++ terms.cmi \
++ orderings.cmi
++index.cmx : \
++ terms.cmx \
++ orderings.cmx \
++ foUtils.cmx \
++ index.cmi
++index.cmi : \
++ terms.cmi \
++ orderings.cmi
++nCicBlob.cmx : \
++ terms.cmx \
++ foUtils.cmx \
++ nCicBlob.cmi
++nCicBlob.cmi : \
++ terms.cmi
++nCicParamod.cmx : \
++ terms.cmx \
++ pp.cmx \
++ paramod.cmx \
++ orderings.cmx \
++ nCicProof.cmx \
++ nCicBlob.cmx \
++ nCicParamod.cmi
++nCicParamod.cmi : \
++ terms.cmi
++nCicProof.cmx : \
++ terms.cmx \
++ pp.cmx \
++ nCicBlob.cmx \
++ foSubst.cmx \
++ nCicProof.cmi
++nCicProof.cmi : \
++ terms.cmi
++orderings.cmx : \
++ terms.cmx \
++ foSubst.cmx \
++ orderings.cmi
++orderings.cmi : \
++ terms.cmi
++paramod.cmx : \
++ terms.cmx \
++ superposition.cmx \
++ pp.cmx \
++ orderings.cmx \
++ index.cmx \
++ foUtils.cmx \
++ paramod.cmi
++paramod.cmi : \
++ terms.cmi \
++ orderings.cmi
++pp.cmx : \
++ terms.cmx \
++ pp.cmi
++pp.cmi : \
++ terms.cmi
++stats.cmx : \
++ terms.cmx \
++ stats.cmi
++stats.cmi : \
++ terms.cmi \
++ orderings.cmi
++superposition.cmx : \
++ terms.cmx \
++ pp.cmx \
++ orderings.cmx \
++ index.cmx \
++ foUtils.cmx \
++ foUnif.cmx \
++ foSubst.cmx \
++ superposition.cmi
++superposition.cmi : \
++ terms.cmi \
++ orderings.cmi \
++ index.cmi
++terms.cmx : \
++ terms.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.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
-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
-paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.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
-nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
- nCicBlob.cmi nCicParamod.cmi
-nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
- nCicBlob.cmx nCicParamod.cmi
- nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \
- nCicMetaSubst.cmi nCicCoercion.cmi
- nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \
- nCicMetaSubst.cmx nCicCoercion.cmi
- nCicCoercion.cmi : nCicUnifHint.cmi
- nCicMetaSubst.cmo : nCicMetaSubst.cmi
- nCicMetaSubst.cmx : nCicMetaSubst.cmi
-nDiscriminationTree.cmi :
++nCicCoercion.cmo : \
++ nDiscriminationTree.cmi \
++ nCicUnifHint.cmi \
++ nCicMetaSubst.cmi \
++ nCicCoercion.cmi
++nCicCoercion.cmx : \
++ nDiscriminationTree.cmx \
++ nCicUnifHint.cmx \
++ nCicMetaSubst.cmx \
++ nCicCoercion.cmi
++nCicCoercion.cmi : \
++ nCicUnifHint.cmi
++nCicMetaSubst.cmo : \
++ nCicMetaSubst.cmi
++nCicMetaSubst.cmx : \
++ nCicMetaSubst.cmi
nCicMetaSubst.cmi :
- nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi
- nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnifHint.cmi :
-nCicCoercion.cmi : nCicUnifHint.cmi
++nCicRefineUtil.cmo : \
++ nCicMetaSubst.cmi \
++ nCicRefineUtil.cmi
++nCicRefineUtil.cmx : \
++ nCicMetaSubst.cmx \
++ nCicRefineUtil.cmi
nCicRefineUtil.cmi :
- nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi nCicRefiner.cmi
- nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.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 \
++nCicRefiner.cmo : \
++ nCicUnification.cmi \
++ nCicRefineUtil.cmi \
++ nCicMetaSubst.cmi \
++ nCicCoercion.cmi \
++ nCicRefiner.cmi
++nCicRefiner.cmx : \
++ nCicUnification.cmx \
++ nCicRefineUtil.cmx \
++ nCicMetaSubst.cmx \
++ nCicCoercion.cmx \
++ nCicRefiner.cmi
++nCicRefiner.cmi : \
++ nCicCoercion.cmi
++nCicUnifHint.cmo : \
++ nDiscriminationTree.cmi \
++ nCicMetaSubst.cmi \
nCicUnifHint.cmi
--nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \
++nCicUnifHint.cmx : \
++ nDiscriminationTree.cmx \
++ nCicMetaSubst.cmx \
nCicUnifHint.cmi
-nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \
- nCicMetaSubst.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
-nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi nCicRefiner.cmi
-nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.cmi
+nCicUnifHint.cmi :
- nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
- nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
- nCicUnification.cmi : nCicCoercion.cmi
- nDiscriminationTree.cmo : nDiscriminationTree.cmi
- nDiscriminationTree.cmx : nDiscriminationTree.cmi
++nCicUnification.cmo : \
++ nCicUnifHint.cmi \
++ nCicMetaSubst.cmi \
++ nCicUnification.cmi
++nCicUnification.cmx : \
++ nCicUnifHint.cmx \
++ nCicMetaSubst.cmx \
++ nCicUnification.cmi
++nCicUnification.cmi : \
++ nCicCoercion.cmi
++nDiscriminationTree.cmo : \
++ nDiscriminationTree.cmi
++nDiscriminationTree.cmx : \
++ nDiscriminationTree.cmi
+nDiscriminationTree.cmi :
- nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \
- nCicMetaSubst.cmx nCicCoercion.cmi
- nCicCoercion.cmi : nCicUnifHint.cmi
- nCicMetaSubst.cmx : nCicMetaSubst.cmi
-nDiscriminationTree.cmi :
++nCicCoercion.cmx : \
++ nDiscriminationTree.cmx \
++ nCicUnifHint.cmx \
++ nCicMetaSubst.cmx \
++ nCicCoercion.cmi
++nCicCoercion.cmi : \
++ nCicUnifHint.cmi
++nCicMetaSubst.cmx : \
++ nCicMetaSubst.cmi
nCicMetaSubst.cmi :
- nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnifHint.cmi :
-nCicCoercion.cmi : nCicUnifHint.cmi
++nCicRefineUtil.cmx : \
++ nCicMetaSubst.cmx \
++ nCicRefineUtil.cmi
nCicRefineUtil.cmi :
- nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.cmi
-nCicUnification.cmi : nCicCoercion.cmi
--nCicRefiner.cmi : nCicCoercion.cmi
- nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \
-nDiscriminationTree.cmo : nDiscriminationTree.cmi
-nDiscriminationTree.cmx : nDiscriminationTree.cmi
-nCicMetaSubst.cmo : nCicMetaSubst.cmi
-nCicMetaSubst.cmx : nCicMetaSubst.cmi
-nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \
++nCicRefiner.cmx : \
++ nCicUnification.cmx \
++ nCicRefineUtil.cmx \
++ nCicMetaSubst.cmx \
++ nCicCoercion.cmx \
++ nCicRefiner.cmi
++nCicRefiner.cmi : \
++ nCicCoercion.cmi
++nCicUnifHint.cmx : \
++ nDiscriminationTree.cmx \
++ nCicMetaSubst.cmx \
nCicUnifHint.cmi
-nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \
- nCicUnifHint.cmi
-nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \
- nCicMetaSubst.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
-nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi nCicRefiner.cmi
-nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.cmi
+nCicUnifHint.cmi :
- nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
- nCicUnification.cmi : nCicCoercion.cmi
- nDiscriminationTree.cmx : nDiscriminationTree.cmi
++nCicUnification.cmx : \
++ nCicUnifHint.cmx \
++ nCicMetaSubst.cmx \
++ nCicUnification.cmi
++nCicUnification.cmi : \
++ nCicCoercion.cmi
++nDiscriminationTree.cmx : \
++ nDiscriminationTree.cmi
+nDiscriminationTree.cmi :
--continuationals.cmo : continuationals.cmi
--continuationals.cmx : continuationals.cmi
++continuationals.cmo : \
++ continuationals.cmi
++continuationals.cmx : \
++ continuationals.cmi
continuationals.cmi :
-declarative.cmo : nnAuto.cmi nTactics.cmi nTacStatus.cmi nCicElim.cmi \
- continuationals.cmi declarative.cmi
-declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \
- continuationals.cmx declarative.cmi
-declarative.cmi : nnAuto.cmi nTacStatus.cmi
--nCicElim.cmo : nCicElim.cmi
--nCicElim.cmx : nCicElim.cmi
++declarative.cmo : \
++ nnAuto.cmi \
++ nTactics.cmi \
++ nTacStatus.cmi \
++ nCicElim.cmi \
++ continuationals.cmi \
++ declarative.cmi
++declarative.cmx : \
++ nnAuto.cmx \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ declarative.cmi
++declarative.cmi : \
++ nnAuto.cmi \
++ nTacStatus.cmi
++nCicElim.cmo : \
++ nCicElim.cmi
++nCicElim.cmx : \
++ nCicElim.cmi
nCicElim.cmi :
--nCicTacReduction.cmo : nCicTacReduction.cmi
--nCicTacReduction.cmx : nCicTacReduction.cmi
++nCicTacReduction.cmo : \
++ nCicTacReduction.cmi
++nCicTacReduction.cmx : \
++ nCicTacReduction.cmi
nCicTacReduction.cmi :
--nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \
++nDestructTac.cmo : \
++ nTactics.cmi \
++ nTacStatus.cmi \
++ continuationals.cmi \
nDestructTac.cmi
--nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
++nDestructTac.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ continuationals.cmx \
nDestructTac.cmi
--nDestructTac.cmi : nTacStatus.cmi
--nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \
-- continuationals.cmi nInversion.cmi
--nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \
-- continuationals.cmx nInversion.cmi
--nInversion.cmi : nTacStatus.cmi
--nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
--nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
--nTacStatus.cmi : continuationals.cmi
--nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
--nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
--nTactics.cmi : nTacStatus.cmi
--nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
-- continuationals.cmi nnAuto.cmi
--nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
-- continuationals.cmx nnAuto.cmi
--nnAuto.cmi : nTacStatus.cmi
++nDestructTac.cmi : \
++ nTacStatus.cmi
++nInversion.cmo : \
++ nTactics.cmi \
++ nTacStatus.cmi \
++ nCicElim.cmi \
++ continuationals.cmi \
++ nInversion.cmi
++nInversion.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ nInversion.cmi
++nInversion.cmi : \
++ nTacStatus.cmi
++nTacStatus.cmo : \
++ nCicTacReduction.cmi \
++ continuationals.cmi \
++ nTacStatus.cmi
++nTacStatus.cmx : \
++ nCicTacReduction.cmx \
++ continuationals.cmx \
++ nTacStatus.cmi
++nTacStatus.cmi : \
++ continuationals.cmi
++nTactics.cmo : \
++ nTacStatus.cmi \
++ nCicElim.cmi \
++ continuationals.cmi \
++ nTactics.cmi
++nTactics.cmx : \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ nTactics.cmi
++nTactics.cmi : \
++ nTacStatus.cmi
++nnAuto.cmo : \
++ nTactics.cmi \
++ nTacStatus.cmi \
++ nCicTacReduction.cmi \
++ continuationals.cmi \
++ nnAuto.cmi
++nnAuto.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicTacReduction.cmx \
++ continuationals.cmx \
++ nnAuto.cmi
++nnAuto.cmi : \
++ nTacStatus.cmi
- continuationals.cmx : continuationals.cmi
++continuationals.cmx : \
++ continuationals.cmi
continuationals.cmi :
- nCicElim.cmx : nCicElim.cmi
-nCicTacReduction.cmi :
-nTacStatus.cmi : continuationals.cmi
++declarative.cmx : \
++ nnAuto.cmx \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ declarative.cmi
++declarative.cmi : \
++ nnAuto.cmi \
++ nTacStatus.cmi
++nCicElim.cmx : \
++ nCicElim.cmi
nCicElim.cmi :
-nTactics.cmi : nTacStatus.cmi
-declarative.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
-declarative.cmo : nTactics.cmi declarative.cmi
-declarative.cmx : nTactics.cmx declarative.cmi
-nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
- continuationals.cmi nnAuto.cmi
-nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
- continuationals.cmx nnAuto.cmi
-nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \
- nDestructTac.cmi
-nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
++nCicTacReduction.cmx : \
++ nCicTacReduction.cmi
+nCicTacReduction.cmi :
- nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
++nDestructTac.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ continuationals.cmx \
nDestructTac.cmi
- nDestructTac.cmi : nTacStatus.cmi
-nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \
- continuationals.cmi nInversion.cmi
--nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \
-- continuationals.cmx nInversion.cmi
- nInversion.cmi : nTacStatus.cmi
- nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
- nTacStatus.cmi : continuationals.cmi
- nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
- nTactics.cmi : nTacStatus.cmi
- nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
- continuationals.cmx nnAuto.cmi
- nnAuto.cmi : nTacStatus.cmi
++nDestructTac.cmi : \
++ nTacStatus.cmi
++nInversion.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ nInversion.cmi
++nInversion.cmi : \
++ nTacStatus.cmi
++nTacStatus.cmx : \
++ nCicTacReduction.cmx \
++ continuationals.cmx \
++ nTacStatus.cmi
++nTacStatus.cmi : \
++ continuationals.cmi
++nTactics.cmx : \
++ nTacStatus.cmx \
++ nCicElim.cmx \
++ continuationals.cmx \
++ nTactics.cmi
++nTactics.cmi : \
++ nTacStatus.cmi
++nnAuto.cmx : \
++ nTactics.cmx \
++ nTacStatus.cmx \
++ nCicTacReduction.cmx \
++ continuationals.cmx \
++ nnAuto.cmi
++nnAuto.cmi : \
++ nTacStatus.cmi
let rec aux acc depth =
function
| [] -> acc
- | (locs, todos, conts, tag) :: tl ->
- | (locs, todos, conts, tag, p) :: tl ->
++ | (locs, todos, conts, tag, _p) :: tl ->
let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in
let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
--- /dev/null
- | (g1, _, k, tag1, _) :: tl ->
+ (* Copyright (C) 2019, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+ open Continuationals.Stack
+ module Ast = NotationPt
+ open NTactics
+ open NTacStatus
+
+ type just = [ `Term of NTacStatus.tactic_term | `Auto of NnAuto.auto_params ]
+
+ let mk_just status goal =
+ function
+ `Auto (l,params) -> NnAuto.auto_lowtac ~params:(l,params) status goal
+ | `Term t -> apply_tac t
+
+ exception NotAProduct
+ exception FirstTypeWrong
+ exception NotEquivalentTypes
+
+ let extract_first_goal_from_status status =
+ let s = status#stack in
+ match s with
+ | [] -> fail (lazy "There's nothing to prove")
- | loc::tl ->
++ | (g1, _, _k, _tag1, _) :: _tl ->
+ let goals = filter_open g1 in
+ match goals with
+ [] -> fail (lazy "No goals under focus")
- let status,gty = term_of_cic_term status gty ctx in
- gty
++ | loc::_tl ->
+ let goal = goal_of_loc (loc) in
+ goal ;;
+
+ let extract_conclusion_type status goal =
+ let gty = get_goalty status goal in
+ let ctx = ctx_of gty in
- | (k,v as hd')::tl' ->
++ term_of_cic_term status gty ctx
+ ;;
+
+ let alpha_eq_tacterm_kerterm ty t status goal =
+ let gty = get_goalty status goal in
+ let ctx = ctx_of gty in
+ let status,cicterm = disambiguate status ctx ty `XTNone (*(`XTSome (mk_cic_term ctx t))*) in
+ let (_,_,metasenv,subst,_) = status#obj in
+ let status,ty = term_of_cic_term status cicterm ctx in
+ if NCicReduction.alpha_eq status metasenv subst ctx t ty then
+ true
+ else
+ false
+ ;;
+
+ let are_convertible ty1 ty2 status goal =
+ let gty = get_goalty status goal in
+ let ctx = ctx_of gty in
+ let status,cicterm1 = disambiguate status ctx ty1 `XTNone in
+ let status,cicterm2 = disambiguate status ctx ty2 `XTNone in
+ NTacStatus.are_convertible status ctx cicterm1 cicterm2
+
+ let clear_volatile_params_tac status =
+ match status#stack with
+ [] -> fail (lazy "Empty stack")
+ | (g,t,k,tag,p)::tl ->
+ let rec remove_volatile = function
+ [] -> []
- | NCic.Prod (_,t,_) ->
++ | (k,_v as hd')::tl' ->
+ let re = Str.regexp "volatile_.*" in
+ if Str.string_match re k 0 then
+ remove_volatile tl'
+ else
+ hd'::(remove_volatile tl')
+ in
+ let newp = remove_volatile p in
+ status#set_stack ((g,t,k,tag,newp)::tl)
+ ;;
+
+ let add_parameter_tac key value status =
+ match status#stack with
+ [] -> status
+ | (g,t,k,tag,p) :: tl -> status#set_stack ((g,t,k,tag,(key,value)::p)::tl)
+ ;;
+
+
+ (* LCF-like tactic that checks whether the conclusion of the sequent of the given goal is a product, checks that
+ the type of the conclusion's bound variable is the same as t1 and then uses an exact_tac with
+ \lambda id: t1. ?. If a t2 is given it checks that t1 ~_{\beta} t2 and uses and exact_tac with \lambda id: t2. ?
+ *)
+ let lambda_abstract_tac id t1 status goal =
+ match extract_conclusion_type status goal with
- let t = extract_conclusion_type status goal in
++ | status,NCic.Prod (_,t,_) ->
+ if alpha_eq_tacterm_kerterm t1 t status goal then
+ let (_,_,t1) = t1 in
+ block_tac [exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit
+ `JustOne))); clear_volatile_params_tac;
+ add_parameter_tac "volatile_newhypo" id] status
+ else
+ raise FirstTypeWrong
+ | _ -> raise NotAProduct
+
+ let assume name ty status =
+ let goal = extract_first_goal_from_status status in
+ try lambda_abstract_tac name ty status goal
+ with
+ | NotAProduct -> fail (lazy "You can't assume without an universal quantification")
+ | FirstTypeWrong -> fail (lazy "The assumed type is wrong")
+ | NotEquivalentTypes -> fail (lazy "The two given types are not equivalent")
+ ;;
+
+ let suppose t1 id status =
+ let goal = extract_first_goal_from_status status in
+ try lambda_abstract_tac id t1 status goal
+ with
+ | NotAProduct -> fail (lazy "You can't suppose without a logical implication")
+ | FirstTypeWrong -> fail (lazy "The supposed proposition is different from the premise")
+ | NotEquivalentTypes -> fail (lazy "The two given propositions are not equivalent")
+ ;;
+
+ let assert_tac t1 t2 status goal continuation =
- let status,res = are_convertible t1 t2 status goal in
++ let status,t = extract_conclusion_type status goal in
+ if alpha_eq_tacterm_kerterm t1 t status goal then
+ match t2 with
+ | None -> continuation
+ | Some t2 ->
- | (g,t,k,tag,p)::_ -> try List.assoc key p with _ -> ""
++ let _status,res = are_convertible t1 t2 status goal in
+ if res then continuation
+ else
+ raise NotEquivalentTypes
+ else
+ raise FirstTypeWrong
+
+ let branch_dot_tac status =
+ match status#stack with
+ ([],t,k,tag,p) :: tl ->
+ if List.length t > 0 then
+ status#set_stack (([List.hd t],List.tl t,k,tag,p)::tl)
+ else
+ status
+ | _ -> status
+ ;;
+
+ let status_parameter key status =
+ match status#stack with
+ [] -> ""
- let wrappedjust = just in
++ | (_g,_t,_k,_tag,p)::_ -> try List.assoc key p with _ -> ""
+ ;;
+
+ let beta_rewriting_step t status =
+ let ctx = status_parameter "volatile_context" status in
+ if ctx <> "beta_rewrite" then
+ (
+ let newhypo = status_parameter "volatile_newhypo" status in
+ if newhypo = "" then
+ fail (lazy "Invalid use of 'or equivalently'")
+ else
+ change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status
+ )
+ else
+ change_tac ~where:("",0,(None,[],Some
+ Ast.UserInput)) ~with_what:t status
+ ;;
+
+ let done_continuation status =
+ let rec continuation l =
+ match l with
+ [] -> []
+ | (_,t,_,tag,p)::tl ->
+ if tag = `BranchTag then
+ if List.length t > 0 then
+ let continue =
+ let ctx =
+ try List.assoc "context" p
+ with Not_found -> ""
+ in
+ ctx <> "induction" && ctx <> "cases"
+ in
+ if continue then [clear_volatile_params_tac;branch_dot_tac] else
+ [clear_volatile_params_tac]
+ else
+ [merge_tac] @ (continuation tl)
+ else
+ []
+ in
+ continuation status#stack
+ ;;
+
+ let bydone just status =
+ let goal = extract_first_goal_from_status status in
+ let continuation = done_continuation status in
+ let l = [mk_just status goal just] @ continuation in
+ block_tac l status
+ ;;
+
+ let push_goals_tac status =
+ match status#stack with
+ [] -> fail (lazy "Error pushing goals")
+ | (g1,t1,k1,tag1,p1) :: (g2,t2,k2,tag2,p2) :: tl ->
+ if List.length g2 > 0 then
+ status#set_stack ((g1,t1 @+ g2,k1,tag1,p1) :: ([],t2,k2,tag2,p2) :: tl)
+ else status (* Nothing to push *)
+ | _ -> status
+
+ let we_need_to_prove t id status =
+ let goal = extract_first_goal_from_status status in
+ match id with
+ | None ->
+ (
+ try assert_tac t None status goal (add_parameter_tac "volatile_context" "beta_rewrite" status)
+ with
+ | FirstTypeWrong -> fail (lazy "The given proposition is not the same as the conclusion")
+ )
+ | Some id ->
+ (
+ block_tac [clear_volatile_params_tac; cut_tac t; branch_tac; shift_tac; intro_tac id; merge_tac; branch_tac;
+ push_goals_tac; add_parameter_tac "volatile_context" "beta_rewrite"
+ ] status
+ )
+ ;;
+
+ let by_just_we_proved just ty id status =
+ let goal = extract_first_goal_from_status status in
- | (k',v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
+ let just = mk_just status goal just in
+ match id with
+ | None ->
+ assert_tac ty None status goal (block_tac [clear_volatile_params_tac; add_parameter_tac
+ "volatile_context" "beta_rewrite"] status)
+ | Some id ->
+ (
+ block_tac [cut_tac ty; branch_tac; just; shift_tac; intro_tac id; merge_tac;
+ clear_volatile_params_tac; add_parameter_tac "volatile_newhypo" id] status
+ )
+ ;;
+
+ let existselim just id1 t1 t2 id2 status =
+ let goal = extract_first_goal_from_status status in
+ let (_,_,t1) = t1 in
+ let (_,_,t2) = t2 in
+ let just = mk_just status goal just in
+ (block_tac [
+ cut_tac ("",0,(Ast.Appl [Ast.Ident ("ex",None); t1; Ast.Binder (`Lambda,(Ast.Ident
+ (id1,None), Some t1),t2)]));
+ branch_tac ~force:false;
+ just;
+ shift_tac;
+ case1_tac "_";
+ intros_tac ~names_ref:(ref []) [id1;id2];
+ merge_tac;
+ clear_volatile_params_tac
+ ]) status
+ ;;
+
+ let andelim just t1 id1 t2 id2 status =
+ let goal = extract_first_goal_from_status status in
+ let (_,_,t1) = t1 in
+ let (_,_,t2) = t2 in
+ let just = mk_just status goal just in
+ (block_tac [
+ cut_tac ("",0,(Ast.Appl [Ast.Ident ("And",None); t1 ; t2]));
+ branch_tac ~force:false;
+ just;
+ shift_tac;
+ case1_tac "_";
+ intros_tac ~names_ref:(ref []) [id1;id2];
+ merge_tac;
+ clear_volatile_params_tac
+ ]) status
+ ;;
+
+ let type_of_tactic_term status ctx t =
+ let status,cicterm = disambiguate status ctx t `XTNone in
+ let (_,cicty) = typeof status ctx cicterm in
+ cicty
+
+ let swap_first_two_goals_tac status =
+ let gstatus =
+ match status#stack with
+ | [] -> assert false
+ | (g,t,k,tag,p) :: s ->
+ match g with
+ | (loc1) :: (loc2) :: tl ->
+ ([loc2;loc1] @+ tl,t,k,tag,p) :: s
+ | _ -> assert false
+ in
+ status#set_stack gstatus
+
+ let thesisbecomes t1 = we_need_to_prove t1 None
+ ;;
+
+ let obtain id t1 status =
+ let goal = extract_first_goal_from_status status in
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let cicty = type_of_tactic_term status ctx t1 in
+ let _,ty = term_of_cic_term status cicty ctx in
+ let (_,_,t1) = t1 in
+ block_tac [ cut_tac ("",0,(Ast.Appl [Ast.Ident ("eq",None); Ast.NCic ty; t1; Ast.Implicit
+ `JustOne]));
+ swap_first_two_goals_tac;
+ branch_tac; shift_tac; shift_tac; intro_tac id; merge_tac; branch_tac; push_goals_tac;
+ add_parameter_tac "volatile_context" "rewrite"
+ ]
+ status
+ ;;
+
+ let conclude t1 status =
+ let goal = extract_first_goal_from_status status in
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let _,gty = term_of_cic_term status cicgty ctx in
+ match gty with
+ (* The first term of this Appl should probably be "eq" *)
+ NCic.Appl [_;_;plhs;_] ->
+ if alpha_eq_tacterm_kerterm t1 plhs status goal then
+ add_parameter_tac "volatile_context" "rewrite" status
+ else
+ fail (lazy "The given conclusion is different from the left-hand side of the current conclusion")
+ | _ -> fail (lazy "Your conclusion needs to be an equality")
+ ;;
+
+ let rewritingstep rhs just last_step status =
+ let ctx = status_parameter "volatile_context" status in
+ if ctx = "rewrite" then
+ (
+ let goal = extract_first_goal_from_status status in
+ let cicgty = get_goalty status goal in
+ let ctx = ctx_of cicgty in
+ let _,gty = term_of_cic_term status cicgty ctx in
+ let cicty = type_of_tactic_term status ctx rhs in
+ let _,ty = term_of_cic_term status cicty ctx in
+ let just' = (* Extraction of the ""justification"" from the ad hoc justification *)
+ match just with
+ `Auto (univ, params) ->
+ let params =
+ if not (List.mem_assoc "timeout" params) then
+ ("timeout","3")::params
+ else params
+ in
+ let params' =
+ if not (List.mem_assoc "paramodulation" params) then
+ ("paramodulation","1")::params
+ else params
+ in
+ if params = params' then NnAuto.auto_lowtac ~params:(univ, params) status goal
+ else
+ first_tac [NnAuto.auto_lowtac ~params:(univ, params) status goal; NnAuto.auto_lowtac
+ ~params:(univ, params') status goal]
+ | `Term just -> apply_tac just
+ | `SolveWith term -> NnAuto.demod_tac ~params:(Some [term], ["all","1";"steps","1"; "use_ctx","false"])
+ | `Proof -> id_tac
+ in
+ let plhs,prhs,prepare =
+ match gty with (* Extracting the lhs and rhs of the previous equality *)
+ NCic.Appl [_;_;plhs;prhs] -> plhs,prhs,(fun continuation -> continuation status)
+ | _ -> fail (lazy "You are not building an equaility chain")
+ in
+ let continuation =
+ if last_step then
+ let todo = [just'] @ (done_continuation status) in
+ block_tac todo
+ else
+ let (_,_,rhs) = rhs in
+ block_tac [apply_tac ("",0,Ast.Appl [Ast.Ident ("trans_eq",None); Ast.NCic ty; Ast.NCic plhs;
+ rhs; Ast.NCic prhs]); branch_tac; just'; merge_tac]
+ in
+ prepare continuation
+ )
+ else
+ fail (lazy "You are not building an equality chain")
+ ;;
+
+ let rec pp_metasenv_names (metasenv:NCic.metasenv) =
+ match metasenv with
+ [] -> ""
+ | hd :: tl ->
+ let n,conj = hd in
+ let meta_attrs,_,_ = conj in
+ let rec find_name_aux meta_attrs = match meta_attrs with
+ [] -> "Anonymous"
+ | hd :: tl -> match hd with
+ `Name n -> n
+ | _ -> find_name_aux tl
+ in
+ let name = find_name_aux meta_attrs
+ in
+ "[Goal: " ^ (string_of_int n) ^ ", Name: " ^ name ^ "]; " ^ (pp_metasenv_names tl)
+ ;;
+
+ let print_goals_names_tac s (status:#NTacStatus.tac_status) =
+ let (_,_,metasenv,_,_) = status#obj in
+ prerr_endline (s ^" -> Metasenv: " ^ (pp_metasenv_names metasenv)); status
+
+ (* Useful as it does not change the order in the list *)
+ let rec list_change_assoc k v = function
+ [] -> []
- let (mattrs,ctx,t as conj) = try List.assoc goal metasenv with _ -> assert false in
++ | (k',_v' as hd) :: tl -> if k' = k then (k',v) :: tl else hd :: (list_change_assoc k v tl)
+ ;;
+
+ let add_names_to_goals_tac (cl:NCic.constructor list ref) (status:#NTacStatus.tac_status) =
+ let add_name_to_goal name goal metasenv =
- | (g,_,_,_,_) :: tl ->
++ let (mattrs,ctx,t) = try List.assoc goal metasenv with _ -> assert false in
+ let mattrs = (`Name name) :: (List.filter (function `Name _ -> false | _ -> true) mattrs) in
+ let newconj = (mattrs,ctx,t) in
+ list_change_assoc goal newconj metasenv
+ in
+ let new_goals =
+ (* It's important that this tactic is called before branching and right after the creation of
+ * the new goals, when they are still under focus *)
+ match status#stack with
+ [] -> fail (lazy "Can not add names to an empty stack")
- | ([],_,_,_,_) :: tl -> false
++ | (g,_,_,_,_) :: _tl ->
+ let rec sublist n = function
+ [] -> []
+ | hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
+ in
+ List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
+ in
+ let rec add_names_to_goals g cl metasenv =
+ match g,cl with
+ [],[] -> metasenv
+ | hd::tl, (_,consname,_)::tl' ->
+ add_names_to_goals tl tl' (add_name_to_goal consname hd metasenv)
+ | _,_ -> fail (lazy "There are less goals than constructors")
+ in
+ let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+ let newmetasenv = add_names_to_goals new_goals !cl metasenv
+ in status#set_obj(olduri,oldint,newmetasenv,oldsubst,oldkind)
+ ;;
+ (*
+ let (olduri,oldint,metasenv,oldsubst,oldkind) = status#obj in
+ let remove_name_from_metaattrs =
+ List.filter (function `Name _ -> false | _ -> true) in
+ let rec add_names_to_metasenv cl metasenv =
+ match cl,metasenv with
+ [],_ -> metasenv
+ | hd :: tl, mhd :: mtl ->
+ let _,consname,_ = hd in
+ let gnum,conj = mhd in
+ let mattrs,ctx,t = conj in
+ let mattrs = [`Name consname] @ (remove_name_from_metaattrs mattrs)
+ in
+ let newconj = mattrs,ctx,t in
+ let newmeta = gnum,newconj in
+ newmeta :: (add_names_to_metasenv tl mtl)
+ | _,[] -> assert false
+ in
+ let newmetasenv = add_names_to_metasenv !cl metasenv in
+ status#set_obj (olduri,oldint,newmetasenv,oldsubst,oldkind)
+ *)
+
+ let unfocus_branch_tac status =
+ match status#stack with
+ [] -> status
+ | (g,t,k,tag,p) :: tl -> status#set_stack (([],g @+ t,k,tag,p)::tl)
+ ;;
+
+ let we_proceed_by_induction_on t1 t2 status =
+ let goal = extract_first_goal_from_status status in
+ let txt,len,t1 = t1 in
+ let t1 = txt, len, Ast.Appl [t1; Ast.Implicit `Vector] in
+ let indtyinfo = ref None in
+ let sort = ref (NCic.Rel 1) in
+ let cl = ref [] in (* this is a ref on purpose, as the block of code after sort_of_goal_tac in
+ block_tac acts as a block of asynchronous code, in which cl gets modified with the info retrieved
+ with analize_indty_tac, and later used to label each new goal with a costructor name. Using a
+ plain list this doesn't seem to work, as add_names_to_goals_tac would immediately act on an empty
+ list, instead of acting on the list of constructors *)
+ try
+ assert_tac t2 None status goal (block_tac [
+ analyze_indty_tac ~what:t1 indtyinfo;
+ sort_of_goal_tac sort;
+ (fun status ->
+ let ity = HExtlib.unopt !indtyinfo in
+ let NReference.Ref (uri, _) = ref_of_indtyinfo ity in
+ let name =
+ NUri.name_of_uri uri ^ "_" ^
+ snd (NCicElim.ast_of_sort
+ (match !sort with NCic.Sort x -> x | _ -> assert false))
+ in
+ let eliminator =
+ let l = [Ast.Ident (name,None)] in
+ (* Generating an implicit for each argument of the inductive type, plus one the
+ * predicate, plus an implicit for each constructor of the inductive type *)
+ let l = l @ HExtlib.mk_list (Ast.Implicit `JustOne) (ity.leftno+1+ity.consno) in
+ let _,_,t1 = t1 in
+ let l = l @ [t1] in
+ Ast.Appl l
+ in
+ cl := ity.cl;
+ exact_tac ("",0,eliminator) status);
+ add_names_to_goals_tac cl;
+ branch_tac;
+ push_goals_tac;
+ unfocus_branch_tac;
+ add_parameter_tac "context" "induction"
+ ] status)
+ with
+ | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+ ;;
+
+ let we_proceed_by_cases_on ((txt,len,ast1) as t1) t2 status =
+ let goal = extract_first_goal_from_status status in
+ let npt1 = txt, len, Ast.Appl [ast1; Ast.Implicit `Vector] in
+ let indtyinfo = ref None in
+ let cl = ref [] in
+ try
+ assert_tac t2 None status goal (block_tac [
+ analyze_indty_tac ~what:npt1 indtyinfo;
+ cases_tac ~what:t1 ~where:("",0,(None,[],Some
+ Ast.UserInput));
+ (
+ fun status ->
+ let ity = HExtlib.unopt !indtyinfo in
+ cl := ity.cl; add_names_to_goals_tac cl status
+ );
+ branch_tac; push_goals_tac;
+ unfocus_branch_tac;
+ add_parameter_tac "context" "cases"
+ ] status)
+ with
+ | FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
+ ;;
+
+ let byinduction t1 id = suppose t1 id ;;
+
+ let name_of_conj conj =
+ let mattrs,_,_ = conj in
+ let rec search_name mattrs =
+ match mattrs with
+ [] -> "Anonymous"
+ | hd::tl ->
+ match hd with
+ `Name n -> n
+ | _ -> search_name tl
+ in
+ search_name mattrs
+
+ let rec loc_of_goal goal l =
+ match l with
+ [] -> fail (lazy "Reached the end")
+ | hd :: tl ->
+ let _,sw = hd in
+ let g = goal_of_switch sw in
+ if g = goal then hd
+ else loc_of_goal goal tl
+ ;;
+
+ let has_focused_goal status =
+ match status#stack with
+ [] -> false
++ | ([],_,_,_,_) :: _tl -> false
+ | _ -> true
+ ;;
+
+ let focus_on_case_tac case status =
+ let (_,_,metasenv,_,_) = status#obj in
+ let rec goal_of_case case metasenv =
+ match metasenv with
+ [] -> fail (lazy "The given case does not exist")
+ | (goal,conj) :: tl ->
+ if name_of_conj conj = case then goal
+ else goal_of_case case tl
+ in
+ let goal_to_focus = goal_of_case case metasenv in
+ let gstatus =
+ match status#stack with
+ [] -> fail (lazy "There is nothing to prove")
+ | (g,t,k,tag,p) :: s ->
+ let loc =
+ try
+ loc_of_goal goal_to_focus t
+ with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
+ context")
+ in
+ let curloc = if has_focused_goal status then
+ let goal = extract_first_goal_from_status status in
+ [loc_of_goal goal g]
+ else []
+ in
+ (((g @- curloc) @+ [loc]),(curloc @+ (t @- [loc])),k,tag,p) :: s
+ in
+ status#set_stack gstatus
+ ;;
+
+ let case id l status =
+ let ctx = status_parameter "context" status in
+ if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
+ induction/cases analysis context")
+ else
+ (
+ if has_focused_goal status then fail (lazy "Finish the current case before switching")
+ else
+ (
+ (*
+ let goal = extract_first_goal_from_status status in
+ let (_,_,metasenv,_,_) = status#obj in
+ let conj = NCicUtils.lookup_meta goal metasenv in
+ let name = name_of_conj conj in
+ *)
+ let continuation =
+ let rec aux l =
+ match l with
+ [] -> [id_tac]
+ | (id,ty)::tl ->
+ (try_tac (assume id ("",0,ty))) :: (aux tl)
+ in
+ aux l
+ in
+ (* if name = id then block_tac continuation status *)
+ (* else *)
+ block_tac ([focus_on_case_tac id] @ continuation) status
+ )
+ )
+ ;;
+
+ let print_stack status = prerr_endline ("PRINT STACK: " ^ (pp status#stack)); id_tac status ;;
+
+ (* vim: ts=2: sw=0: et:
+ * *)
status, (ctx, t)
;;
- let n,h,metasenv,subst,o = status#obj in
+ let are_convertible status ctx a b =
+ let status, (_,a) = relocate status ctx a in
+ let status, (_,b) = relocate status ctx b in
++ let _n,_h,metasenv,subst,_o = status#obj in
+ let res = NCicReduction.are_convertible status metasenv subst ctx a b in
+ status, res
+ ;;
+ let are_convertible a b c d = wrap "are_convertible" (are_convertible a b c) d;;
+
let unify status ctx a b =
let status, (_,a) = relocate status ctx a in
let status, (_,b) = relocate status ctx b in
let goalty = get_goalty status goal in
let status, what = disambiguate status (ctx_of goalty) what `XTInd in
let status, ty_what = typeof status (ctx_of what) what in
- let _status, (r,consno,lefts,rights) = analyse_indty status ty_what in
- let status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in
++ let _status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in
let leftno = List.length lefts in
let rightno = List.length rights in
indtyref := Some {
let assert_tac seqs status =
match status#stack with
| [] -> assert false
- | (g,_,_,_) :: _s ->
- | (g,_,_,_,_) :: s ->
++ | (g,_,_,_,_) :: _s ->
assert (List.length g = List.length seqs);
(match seqs with
[] -> id_tac
| NCicTypeChecker.TypeCheckerFailure _
| NCicTypeChecker.AssertFailure _ -> eq_cache)
eq_cache ctx
+ end
;;
- let index_local_equations2 eq_cache status open_goal lemmas nohyps =
-let index_local_equations2 eq_cache status open_goal lemmas ?(flag=false) nohyps =
++let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohyps =
noprint (lazy "indexing equations");
let eq_cache,lemmas =
match lemmas with
cands, diff more_cands cands
;;
-let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
+ let is_a_needed_uri s =
+ s = "cic:/matita/basics/logic/eq.ind" ||
+ s = "cic:/matita/basics/logic/sym_eq.con" ||
+ s = "cic:/matita/basics/logic/trans_eq.con" ||
+ s = "cic:/matita/basics/logic/eq_f3.con" ||
+ s = "cic:/matita/basics/logic/eq_f2.con" ||
+ s = "cic:/matita/basics/logic/eq_f.con"
+
+let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gty =
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let _, raw_gty = term_of_cic_term status gty context in
- let is_prod, is_eq =
+ let is_prod, _is_eq =
- let status, t = term_of_cic_term status gty context in
- let t = NCicReduction.whd status subst context t in
- match t with
- | NCic.Prod _ -> true, false
- | _ -> false, NCicParamod.is_equation status metasenv subst context t
+ let status, t = term_of_cic_term status gty context in
+ let t = NCicReduction.whd status subst context t in
+ match t with
+ | NCic.Prod _ -> true, false
+ | _ -> false, NCicParamod.is_equation status metasenv subst context t
in
debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
let is_eq =
in
let others = menv_closure status (stack_goals (level-1) tl) in
List.for_all (fun i -> IntSet.mem i others)
- (HExtlib.filter_map is_open g)
+ (HExtlib.filter_map is_open g)
- let top_cache ~depth:_ top status cache =
-let top_cache ~depth top status ?(use_given_only=false) cache =
++let top_cache ~depth:_ top status ?(use_given_only=false) cache =
if top then
- let unit_eq = index_local_equations status#eq_cache status in
+ let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in
{cache with unit_eq = unit_eq}
else cache
and
(* BRAND NEW VERSION *)
- auto_main flags signature cache depth status: unit =
-auto_main flags signature cache depth status ?(use_given_only=false): unit=
++auto_main flags signature cache depth ?(use_given_only=false) status: unit=
debug_print ~depth (lazy "entering auto main");
debug_print ~depth (pptrace status cache.trace);
debug_print ~depth (lazy ("stack length = " ^
match goals with
| [] when depth = 0 -> raise (Proved (status,cache.trace))
| [] ->
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache *)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status ~use_given_only
- | orig::_ ->
- if depth > 0 && move_to_side depth status
- then
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache*)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status ~use_given_only
- else
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache *)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
- auto_clusters flags signature cache (depth-1) status
++ auto_clusters flags signature cache (depth-1) status ~use_given_only
+ | _orig::_ ->
+ if depth > 0 && move_to_side depth status
+ then
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> cache (* possible because of intros that cleans the cache*)
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
- auto_clusters flags signature cache (depth-1) status
++ auto_clusters flags signature cache (depth-1) status ~use_given_only
+ else
let ng = List.length goals in
(* moved inside auto_clusters *)
if ng > flags.maxwidth then begin
s
;;
-let auto_lowtac ~params:(univ,flags as params) status goal =
+ let candidates_from_ctx univ ctx status =
+ match univ with
+ | None -> None
+ | Some l ->
+ let to_Ast t =
+ (* FG: `XTSort here? *)
+ let status, res = disambiguate status ctx t `XTNone in
+ let _,res = term_of_cic_term status res (ctx_of res)
+ in Ast.NCic res
+ in Some ((List.map to_Ast l) @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
+ Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
+ Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
+ Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
+ ])
+
++let auto_lowtac ~params:(univ,flags) status goal =
+ let gty = get_goalty status goal in
+ let ctx = ctx_of gty in
+ let candidates = candidates_from_ctx univ ctx status in
+ auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref [])
+
+ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
+ let candidates = candidates_from_ctx univ [] status in
+ auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref status
+
let auto_tac ~params:(_,flags as params) ?trace_ref =
if List.mem_assoc "demod" flags then
demod_tac ~params
- helm_registry.cmo : helm_registry.cmi
- helm_registry.cmx : 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.cmx : 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.cmx : 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
- extThread.cmo : extThread.cmi
- extThread.cmx : extThread.cmi
-threadSafe.cmi :
++extThread.cmo : \
++ extThread.cmi
++extThread.cmx : \
++ extThread.cmi
extThread.cmi :
--threadSafe.cmo : threadSafe.cmi
--threadSafe.cmx : threadSafe.cmi
-extThread.cmo : extThread.cmi
-extThread.cmx : extThread.cmi
++threadSafe.cmo : \
++ threadSafe.cmi
++threadSafe.cmx : \
++ threadSafe.cmi
+threadSafe.cmi :
- extThread.cmx : extThread.cmi
-threadSafe.cmi :
++extThread.cmx : \
++ extThread.cmi
extThread.cmi :
-threadSafe.cmo : threadSafe.cmi
--threadSafe.cmx : threadSafe.cmi
-extThread.cmo : extThread.cmi
-extThread.cmx : extThread.cmi
++threadSafe.cmx : \
++ threadSafe.cmi
+threadSafe.cmi :
- xml.cmo : xml.cmi
- xml.cmx : xml.cmi
++xml.cmo : \
++ xml.cmi
++xml.cmx : \
++ xml.cmi
xml.cmi :
- xmlPushParser.cmo : xmlPushParser.cmi
- xmlPushParser.cmx : xmlPushParser.cmi
++xmlPushParser.cmo : \
++ xmlPushParser.cmi
++xmlPushParser.cmx : \
++ xmlPushParser.cmi
xmlPushParser.cmi :
-xml.cmo : xml.cmi
-xml.cmx : xml.cmi
-xmlPushParser.cmo : xmlPushParser.cmi
-xmlPushParser.cmx : xmlPushParser.cmi
- xml.cmx : xml.cmi
++xml.cmx : \
++ xml.cmi
xml.cmi :
- xmlPushParser.cmx : xmlPushParser.cmi
++xmlPushParser.cmx : \
++ xmlPushParser.cmi
xmlPushParser.cmi :
-xml.cmo : xml.cmi
-xml.cmx : xml.cmi
-xmlPushParser.cmo : xmlPushParser.cmi
-xmlPushParser.cmx : xmlPushParser.cmi
(* $Id$ *)
-open GrafiteTypes
+ module G = GrafiteAst
open Printf
class status baseuri =
let slash_n_RE = Pcre.regexp "\\n" ;;
- let pp_ast_statement status stm =
- let stm = GrafiteAstPp.pp_statement status stm
- ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ let first_line = ref true ;;
+
+ let cases_or_induction_context stack =
+ match stack with
+ [] -> false
- | (g,t,k,tag,p)::tl -> try
++ | (_g,_t,_k,_tag,p)::_tl -> try
+ let s = List.assoc "context" p in
+ s = "cases" || s = "induction"
+ with
+ Not_found -> false
+ ;;
+
+ let has_focused_goal stack =
+ match stack with
+ [] -> false
- | (g,t,k,tag,p)::tl -> (List.length g) > 0
++ | (g,_t,_k,_tag,_p)::_tl -> (List.length g) > 0
+ ;;
+
-let get_indentation status statement =
++let get_indentation status _statement =
+ let base_ind =
+ match status#stack with
+ [] -> 0
+ | s -> List.length(s) * 2
in
- let stm = Pcre.replace ~rex:slash_n_RE stm in
- let stm =
+ if cases_or_induction_context status#stack then
+ (
+ if has_focused_goal status#stack then
+ base_ind + 2
+ else
+ base_ind
+ )
+ else
+ base_ind
+ ;;
+
+ let pp_ind s n =
+ let rec aux s n =
+ match n with
+ 0 -> s
+ | n -> " " ^ (aux s (n-1))
+ in
+ aux s n
+
+ let write_ast_to_file status fname statement =
+ let indentation = get_indentation status statement in
+ let str = match statement with
+ G.Comment _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | G.Executable (_,code) ->
+ (
+ match code with
+ G.NTactic _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | G.NCommand (_,cmd) ->
+ (
+ match cmd with
+ | G.NObj (_,obj,_) ->
+ (
+ match obj with
- Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
++ NotationPt.Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | _ -> ""
+ )
+ | G.NQed _ -> GrafiteAstPp.pp_statement status statement
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ | _ -> ""
+ )
+ | _ -> ""
+ )
+ in
+ if str <> "" then
+ (
+ let s = pp_ind str indentation in
+ let flaglist = if !first_line = false then [Open_wronly; Open_append; Open_creat]
+ else (first_line := false; [Open_wronly; Open_trunc; Open_creat])
+ in
+ let out_channel =
+ Stdlib.open_out_gen flaglist 0o0644 fname in
+ let _ = Stdlib.output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in
+ let _ = Stdlib.close_out out_channel in
+ str
+ )
+ else
+ str
+ ;;
+
+ let pp_ast_statement status stm ~fname =
+ let stm = write_ast_to_file status (fname ^ ".parsed.ma") stm in
+ if stm <> "" then
+ (
+ let stm = Pcre.replace ~rex:slash_n_RE stm in
+ let stm =
if String.length stm > 50 then String.sub stm 0 50 ^ " ..."
else stm
- in
+ in
HLog.debug ("Executing: ``" ^ stm ^ "''")
+ )
+ else
+ HLog.debug ("Executing: `` Unprintable statement ''")
;;
let clean_exit baseuri exn =
(* given a path to a ma file inside the include_paths, returns the
new include_paths associated to that file *)
-let read_include_paths ~include_paths file =
- try
- let root, _buri, _fname, _tgt =
- Librarian.baseuri_of_script ~include_paths:[] file in
- let includes =
- try
- Str.split (Str.regexp " ")
- (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
- with Not_found -> []
- in
- let rc = root :: includes in
+let read_include_paths ~include_paths:_ file =
+ try
+ let root, _buri, _fname, _tgt =
+ Librarian.baseuri_of_script ~include_paths:[] file in
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
+ in
+ let rc = root :: includes in
List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
- []
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ []
;;
- let rec get_ast status ~compiling ~asserted ~include_paths strm =
+ let rec get_ast status ~compiling ~asserted ~include_paths strm =
match GrafiteParser.parse_statement status strm with
- (GrafiteAst.Executable
+ (GrafiteAst.Executable
(_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
- ->
- let already_included = NCicLibrary.get_transitively_included status in
- let asserted,_ =
- assert_ng ~already_included ~compiling ~asserted ~include_paths
- mafilename
- in
- asserted,cmd
- | cmd -> asserted,cmd
+ ->
+ let already_included = NCicLibrary.get_transitively_included status in
+ let asserted,_ =
+ assert_ng ~already_included ~compiling ~asserted ~include_paths
+ mafilename
+ in
+ asserted,cmd
+ | cmd -> asserted,cmd
and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
- let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status str =
- let asserted,stop,status,str =
- try
- let cont =
- try Some (get_ast status ~compiling ~asserted ~include_paths str)
- with End_of_file -> None in
- match cont with
- | None -> asserted, true, status, str
- | Some (asserted,ast) ->
- cb status ast;
- let new_statuses =
- eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
- let status =
- match new_statuses with
- [s,None] -> s
- | _::(_,Some (_,value))::_ ->
- raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
- | _ -> assert false in
- (* CSC: complex patch to re-build the lexer since the tokens may
- have changed. Note: this way we loose look-ahead tokens.
- Hence the "include" command must be terminated (no look-ahead) *)
- let str =
- match ast with
- (GrafiteAst.Executable
- (_,GrafiteAst.NCommand
- (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let rec loop asserted status str =
+ let asserted,stop,status,str =
+ try
+ let cont =
+ try Some (get_ast status ~compiling ~asserted ~include_paths str)
+ with End_of_file -> None in
+ match cont with
+ | None -> asserted, true, status, str
+ | Some (asserted,ast) ->
+ cb status ast;
+ let new_statuses =
+ eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
+ let status =
+ match new_statuses with
+ [s,None] -> s
+ | _::(_,Some (_,value))::_ ->
+ raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
+ | _ -> assert false in
+ (* CSC: complex patch to re-build the lexer since the tokens may
+ have changed. Note: this way we loose look-ahead tokens.
+ Hence the "include" command must be terminated (no look-ahead) *)
+ let str =
+ match ast with
+ (GrafiteAst.Executable
+ (_,GrafiteAst.NCommand
+ (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
GrafiteParser.parsable_statement status
- (GrafiteParser.strm_of_parsable str)
- | _ -> str
- in
- asserted, false, status, str
- with exn when not matita_debug ->
- raise (EnrichedWithStatus (exn, status))
+ (GrafiteParser.strm_of_parsable str)
+ | _ -> str
+ in
+ asserted, false, status, str
+ with exn when not matita_debug ->
+ raise (EnrichedWithStatus (exn, status))
+ in
+ if stop then asserted,status else loop asserted status str
in
- if stop then asserted,status else loop asserted status str
- in
loop asserted status str
and compile ~compiling ~asserted ~include_paths fname =
projects / helm.git / commitdiff