-content.cmi:
-notationUtil.cmi: notationPt.cmx
-notationEnv.cmi: notationPt.cmx
-notationPp.cmi: notationPt.cmx notationEnv.cmi
-notationPt.cmo:
-notationPt.cmx:
-content.cmo: content.cmi
-content.cmx: content.cmi
-notationUtil.cmo: notationPt.cmx notationUtil.cmi
-notationUtil.cmx: notationPt.cmx notationUtil.cmi
-notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi
-notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi
-notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi
+content.cmi:
+notationUtil.cmi: notationPt.cmx
+notationEnv.cmi: notationPt.cmx
+notationPp.cmi: notationPt.cmx notationEnv.cmi
+notationPt.cmo:
+notationPt.cmx:
+content.cmo: content.cmi
+content.cmx: content.cmi
+notationUtil.cmo: notationPt.cmx notationUtil.cmi
+notationUtil.cmx: notationPt.cmx notationUtil.cmi
+notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi
+notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi
+notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi
+notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi
-renderingAttrs.cmi:
-cicNotationLexer.cmi:
-cicNotationParser.cmi:
-mpresentation.cmi:
-box.cmi:
-content2presMatcher.cmi:
-termContentPres.cmi: cicNotationParser.cmi
-boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
-cicNotationPres.cmi: mpresentation.cmi box.cmi
-content2pres.cmi: termContentPres.cmi cicNotationPres.cmi
-renderingAttrs.cmo: renderingAttrs.cmi
-renderingAttrs.cmx: renderingAttrs.cmi
-cicNotationLexer.cmo: cicNotationLexer.cmi
-cicNotationLexer.cmx: cicNotationLexer.cmi
-cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi
-cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi
-mpresentation.cmo: mpresentation.cmi
-mpresentation.cmx: mpresentation.cmi
-box.cmo: renderingAttrs.cmi box.cmi
-box.cmx: renderingAttrs.cmx box.cmi
-content2presMatcher.cmo: content2presMatcher.cmi
-content2presMatcher.cmx: content2presMatcher.cmi
+renderingAttrs.cmi:
+cicNotationLexer.cmi:
+cicNotationParser.cmi:
+mpresentation.cmi:
+box.cmi:
+content2presMatcher.cmi:
+termContentPres.cmi: cicNotationParser.cmi
+boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
+cicNotationPres.cmi: mpresentation.cmi box.cmi
+content2pres.cmi: termContentPres.cmi cicNotationPres.cmi
+renderingAttrs.cmo: renderingAttrs.cmi
+renderingAttrs.cmx: renderingAttrs.cmi
+cicNotationLexer.cmo: cicNotationLexer.cmi
+cicNotationLexer.cmx: cicNotationLexer.cmi
+cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi
+cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi
+mpresentation.cmo: mpresentation.cmi
+mpresentation.cmx: mpresentation.cmi
+box.cmo: renderingAttrs.cmi box.cmi
+box.cmx: renderingAttrs.cmx box.cmi
+content2presMatcher.cmo: content2presMatcher.cmi
+content2presMatcher.cmx: content2presMatcher.cmi
termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \
- cicNotationParser.cmi termContentPres.cmi
+ cicNotationParser.cmi termContentPres.cmi
termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \
- cicNotationParser.cmx termContentPres.cmi
+ cicNotationParser.cmx termContentPres.cmi
boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
- boxPp.cmi
+ boxPp.cmi
boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
- boxPp.cmi
+ boxPp.cmi
cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
- cicNotationPres.cmi
+ cicNotationPres.cmi
cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
- cicNotationPres.cmi
+ cicNotationPres.cmi
content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
- cicNotationPres.cmi box.cmi content2pres.cmi
+ cicNotationPres.cmi box.cmi content2pres.cmi
content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
- cicNotationPres.cmx box.cmx content2pres.cmi
+ cicNotationPres.cmx box.cmx content2pres.cmi
-disambiguateTypes.cmi:
-disambiguate.cmi: disambiguateTypes.cmi
-multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
-disambiguateTypes.cmo: disambiguateTypes.cmi
-disambiguateTypes.cmx: disambiguateTypes.cmi
-disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi
-disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi
+disambiguateTypes.cmi:
+disambiguate.cmi: disambiguateTypes.cmi
+multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
+disambiguateTypes.cmo: disambiguateTypes.cmi
+disambiguateTypes.cmx: disambiguateTypes.cmi
+disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi
+disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi
multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \
- multiPassDisambiguator.cmi
+ multiPassDisambiguator.cmi
multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \
- multiPassDisambiguator.cmi
+ multiPassDisambiguator.cmi
-componentsConf.cmi:
-hExtlib.cmi:
-hMarshal.cmi:
-patternMatcher.cmi:
-hLog.cmi:
-trie.cmi:
-discrimination_tree.cmi:
-hTopoSort.cmi:
-graphvizPp.cmi:
-componentsConf.cmo: componentsConf.cmi
-componentsConf.cmx: componentsConf.cmi
-hExtlib.cmo: hExtlib.cmi
-hExtlib.cmx: hExtlib.cmi
-hMarshal.cmo: hExtlib.cmi hMarshal.cmi
-hMarshal.cmx: hExtlib.cmx hMarshal.cmi
-patternMatcher.cmo: patternMatcher.cmi
-patternMatcher.cmx: patternMatcher.cmi
-hLog.cmo: hLog.cmi
-hLog.cmx: hLog.cmi
-trie.cmo: trie.cmi
-trie.cmx: trie.cmi
-discrimination_tree.cmo: trie.cmi discrimination_tree.cmi
-discrimination_tree.cmx: trie.cmx discrimination_tree.cmi
-hTopoSort.cmo: hTopoSort.cmi
-hTopoSort.cmx: hTopoSort.cmi
-graphvizPp.cmo: graphvizPp.cmi
-graphvizPp.cmx: graphvizPp.cmi
+componentsConf.cmi:
+hExtlib.cmi:
+hMarshal.cmi:
+patternMatcher.cmi:
+hLog.cmi:
+trie.cmi:
+discrimination_tree.cmi:
+hTopoSort.cmi:
+graphvizPp.cmi:
+componentsConf.cmo: componentsConf.cmi
+componentsConf.cmx: componentsConf.cmi
+hExtlib.cmo: hExtlib.cmi
+hExtlib.cmx: hExtlib.cmi
+hMarshal.cmo: hExtlib.cmi hMarshal.cmi
+hMarshal.cmx: hExtlib.cmx hMarshal.cmi
+patternMatcher.cmo: patternMatcher.cmi
+patternMatcher.cmx: patternMatcher.cmi
+hLog.cmo: hLog.cmi
+hLog.cmx: hLog.cmi
+trie.cmo: trie.cmi
+trie.cmx: trie.cmi
+discrimination_tree.cmo: trie.cmi hExtlib.cmi discrimination_tree.cmi
+discrimination_tree.cmx: trie.cmx hExtlib.cmx discrimination_tree.cmi
+hTopoSort.cmo: hTopoSort.cmi
+hTopoSort.cmx: hTopoSort.cmi
+graphvizPp.cmo: graphvizPp.cmi
+graphvizPp.cmx: graphvizPp.cmi
-http_getter_wget.cmi:
-http_getter_logger.cmi:
-http_getter_misc.cmi:
-http_getter_const.cmi:
-http_getter_env.cmi: http_getter_types.cmx
-http_getter_storage.cmi:
-http_getter_common.cmi: http_getter_types.cmx
-http_getter.cmi: http_getter_types.cmx
-http_getter_types.cmo:
-http_getter_types.cmx:
-http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi
-http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi
-http_getter_logger.cmo: http_getter_logger.cmi
-http_getter_logger.cmx: http_getter_logger.cmi
-http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi
-http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi
-http_getter_const.cmo: http_getter_const.cmi
-http_getter_const.cmx: http_getter_const.cmi
+http_getter_wget.cmi:
+http_getter_logger.cmi:
+http_getter_misc.cmi:
+http_getter_const.cmi:
+http_getter_env.cmi: http_getter_types.cmx
+http_getter_storage.cmi:
+http_getter_common.cmi: http_getter_types.cmx
+http_getter.cmi: http_getter_types.cmx
+http_getter_types.cmo:
+http_getter_types.cmx:
+http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi
+http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi
+http_getter_logger.cmo: http_getter_logger.cmi
+http_getter_logger.cmx: http_getter_logger.cmi
+http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi
+http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi
+http_getter_const.cmo: http_getter_const.cmi
+http_getter_const.cmx: http_getter_const.cmi
http_getter_env.cmo: http_getter_types.cmx http_getter_misc.cmi \
- http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi
+ http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi
http_getter_env.cmx: http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
+ http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
http_getter_storage.cmo: http_getter_wget.cmi http_getter_types.cmx \
- http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi
+ http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi
http_getter_storage.cmx: http_getter_wget.cmx http_getter_types.cmx \
- http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
+ http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
http_getter_common.cmo: http_getter_types.cmx http_getter_misc.cmi \
- http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi
+ http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi
http_getter_common.cmx: http_getter_types.cmx http_getter_misc.cmx \
- http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
+ http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
http_getter.cmo: http_getter_wget.cmi http_getter_types.cmx \
http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \
http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \
- http_getter.cmi
+ http_getter.cmi
http_getter.cmx: http_getter_wget.cmx http_getter_types.cmx \
http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
- http_getter.cmi
+ http_getter.cmi
-grafiteAstPp.cmi: grafiteAst.cmx
-grafiteAst.cmo:
-grafiteAst.cmx:
-grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi
-grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
+grafiteAstPp.cmi: grafiteAst.cmx
+grafiteAst.cmo:
+grafiteAst.cmx:
+grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi
+grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
-grafiteTypes.cmi:
-nCicCoercDeclaration.cmi: grafiteTypes.cmi
-grafiteEngine.cmi: grafiteTypes.cmi
-grafiteTypes.cmo: grafiteTypes.cmi
-grafiteTypes.cmx: grafiteTypes.cmi
-nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi
-nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi
+grafiteTypes.cmi:
+nCicCoercDeclaration.cmi: grafiteTypes.cmi
+grafiteEngine.cmi: grafiteTypes.cmi
+grafiteTypes.cmo: grafiteTypes.cmi
+grafiteTypes.cmx: grafiteTypes.cmi
+nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi
+nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi
grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \
- grafiteEngine.cmi
+ grafiteEngine.cmi
grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \
- grafiteEngine.cmi
+ grafiteEngine.cmi
-dependenciesParser.cmi:
-grafiteParser.cmi:
-print_grammar.cmi: grafiteParser.cmi
-dependenciesParser.cmo: dependenciesParser.cmi
-dependenciesParser.cmx: dependenciesParser.cmi
-grafiteParser.cmo: grafiteParser.cmi
-grafiteParser.cmx: grafiteParser.cmi
-print_grammar.cmo: print_grammar.cmi
-print_grammar.cmx: print_grammar.cmi
+grafiteParser.cmi:
+print_grammar.cmi: grafiteParser.cmi
+grafiteParser.cmo: grafiteParser.cmi
+grafiteParser.cmx: grafiteParser.cmi
+print_grammar.cmo: print_grammar.cmi
+print_grammar.cmx: print_grammar.cmi
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90" -> t ] ];
-(* MATITA 1.0
- new_name: [
- [ SYMBOL "_" -> None
- | id = IDENT -> Some id ]
- ];
-*)
ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
tactic_term_list1: [
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
[ IDENT "normalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
let delta = match delta with None -> true | _ -> false in
`Normalize delta
- (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
| IDENT "whd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
let delta = match delta with None -> true | _ -> false in
`Whd delta]
];
pattern_spec: [
[ res = OPT [
- "in";
+ SYMBOL "{";
wanted_and_sps =
[ "match" ; wanted = tactic_term ;
sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
Some wanted,sps
| sps = sequent_pattern_spec ->
None,Some sps
- ] ->
+ ];
+ SYMBOL "}" ->
let wanted,hyp_paths,goal_path =
match wanted_and_sps with
wanted,None -> wanted, [], Some N.UserInput
| SYMBOL "<" -> `RightToLeft ]
];
int: [ [ num = NUMBER -> int_of_string num ] ];
-(* MATITA 1.0
- intros_spec: [
- [ OPT [ IDENT "names" ];
- num = OPT [ num = int -> num ];
- idents = intros_names ->
- num, idents
- ]
- ];
-*)
-(* MATITA 1.0 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; *)
ntactic: [
[ SYMBOL "@"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
- | IDENT "apply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
| IDENT "applyS"; t = tactic_term -> G.NTactic(loc,[G.NSmartApply(loc, t)])
| IDENT "assert";
seqs = LIST0 [
SYMBOL <:unicode<vdash>>;
concl = tactic_term -> (List.rev hyps,concl) ] ->
G.NTactic(loc,[G.NAssert (loc, seqs)])
- (*| IDENT "auto"; params = auto_params ->
- G.NTactic(loc,[G.NAuto (loc, params)])*)
| SYMBOL "/"; num = OPT NUMBER ;
just_and_params = auto_params; SYMBOL "/" ->
let just,params = just_and_params in
| Some `Trace ->
G.NMacro(loc,
G.NAutoInteractive (loc, (None,["depth",depth]@params))))
- | IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc)
- | IDENT "check"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
+ | SYMBOL "#"; SYMBOL "#" -> G.NMacro (loc, G.NIntroGuess loc)
+ | IDENT "check"; t = tactic_term -> G.NMacro(loc,G.NCheck (loc,t))
| IDENT "screenshot"; fname = QSTRING ->
G.NMacro(loc,G.Screenshot (loc, fname))
| IDENT "cases"; what = tactic_term ; where = pattern_spec ->
G.NTactic(loc,[G.NCases (loc, what, where)])
| IDENT "change"; what = pattern_spec; "with"; with_what = tactic_term ->
G.NTactic(loc,[G.NChange (loc, what, with_what)])
- | SYMBOL "-"; ids = LIST1 IDENT ->
- G.NTactic(loc,[G.NClear (loc, ids)])
- | (*SYMBOL "^"*)PLACEHOLDER; num = OPT NUMBER;
+ | SYMBOL "-"; id = IDENT ->
+ G.NTactic(loc,[G.NClear (loc, [id])])
+ | PLACEHOLDER; num = OPT NUMBER;
l = OPT [ SYMBOL "{"; l = LIST1 tactic_term; SYMBOL "}" -> l ] ->
G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),match l with None -> [] | Some l -> l)])
| IDENT "cut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
-(* | IDENT "discriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
- | IDENT "subst"; t = tactic_term -> G.NSubst (loc, t) *)
| IDENT "destruct"; just = OPT [ dom = ident_list1 -> dom ];
exclude = OPT [ IDENT "skip"; skip = ident_list1 -> skip ]
-> let exclude' = match exclude with None -> [] | Some l -> l in
G.NTactic(loc,[G.NReduce (loc, kind, p)])
| dir = direction; what = tactic_term ; where = pattern_spec ->
G.NTactic(loc,[G.NRewrite (loc, dir, what, where)])
- | IDENT "rewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
- G.NTactic(loc,[G.NRewrite (loc, dir, what, where)])
| IDENT "try"; tac = SELF ->
let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
G.NTactic(loc,[ G.NTry (loc,tac)])
| SYMBOL "#"; ns=IDENT -> G.NTactic(loc,[ G.NIntros (loc,[ns])])
| SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
| SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
- | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
+ | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
]
];
auto_fixed_param: [
-librarian.cmi:
-libraryMisc.cmi:
-libraryClean.cmi:
-librarian.cmo: librarian.cmi
-librarian.cmx: librarian.cmi
-libraryMisc.cmo: libraryMisc.cmi
-libraryMisc.cmx: libraryMisc.cmi
-libraryClean.cmo: libraryMisc.cmi libraryClean.cmi
-libraryClean.cmx: libraryMisc.cmx libraryClean.cmi
+librarian.cmi:
+libraryMisc.cmi:
+libraryClean.cmi:
+librarian.cmo: librarian.cmi
+librarian.cmx: librarian.cmi
+libraryMisc.cmo: libraryMisc.cmi
+libraryMisc.cmx: libraryMisc.cmi
+libraryClean.cmo: libraryClean.cmi
+libraryClean.cmx: libraryClean.cmi
-helmLogger.cmi:
-helmLogger.cmo: helmLogger.cmi
-helmLogger.cmx: helmLogger.cmi
+helmLogger.cmi:
+helmLogger.cmo: helmLogger.cmi
+helmLogger.cmx: helmLogger.cmi
-ncic2astMatcher.cmi:
-interpretations.cmi:
-ncic2astMatcher.cmo: ncic2astMatcher.cmi
-ncic2astMatcher.cmx: ncic2astMatcher.cmi
-interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi
-interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi
+ncic2astMatcher.cmi:
+interpretations.cmi:
+ncic2astMatcher.cmo: ncic2astMatcher.cmi
+ncic2astMatcher.cmx: ncic2astMatcher.cmi
+interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi
+interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi
-nnumber_notation.cmi:
-disambiguateChoices.cmi:
-nCicDisambiguate.cmi:
-grafiteDisambiguate.cmi:
-nnumber_notation.cmo: nnumber_notation.cmi
-nnumber_notation.cmx: nnumber_notation.cmi
-disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi
-disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi
-nCicDisambiguate.cmo: nCicDisambiguate.cmi
-nCicDisambiguate.cmx: nCicDisambiguate.cmi
+nnumber_notation.cmi:
+disambiguateChoices.cmi:
+nCicDisambiguate.cmi:
+grafiteDisambiguate.cmi:
+nnumber_notation.cmo: nnumber_notation.cmi
+nnumber_notation.cmx: nnumber_notation.cmi
+disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi
+disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi
+nCicDisambiguate.cmo: nCicDisambiguate.cmi
+nCicDisambiguate.cmx: nCicDisambiguate.cmi
grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \
- grafiteDisambiguate.cmi
+ grafiteDisambiguate.cmi
grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \
- grafiteDisambiguate.cmi
+ grafiteDisambiguate.cmi
-nUri.cmi:
-nReference.cmi: nUri.cmi
-nCicUtils.cmi: nCic.cmx
-nCicSubstitution.cmi: nCic.cmx
-nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx
-nCicReduction.cmi: nCic.cmx
-nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx
-nCicUntrusted.cmi: nCic.cmx
-nCicPp.cmi: nReference.cmi nCic.cmx
-nCic.cmo: nUri.cmi nReference.cmi
-nCic.cmx: nUri.cmx nReference.cmx
-nUri.cmo: nUri.cmi
-nUri.cmx: nUri.cmi
-nReference.cmo: nUri.cmi nReference.cmi
-nReference.cmx: nUri.cmx nReference.cmi
-nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi
-nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi
+nUri.cmi:
+nReference.cmi: nUri.cmi
+nCicUtils.cmi: nCic.cmx
+nCicSubstitution.cmi: nCic.cmx
+nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx
+nCicReduction.cmi: nCic.cmx
+nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx
+nCicUntrusted.cmi: nCic.cmx
+nCicPp.cmi: nReference.cmi nCic.cmx
+nCic.cmo: nUri.cmi nReference.cmi
+nCic.cmx: nUri.cmx nReference.cmx
+nUri.cmo: nUri.cmi
+nUri.cmx: nUri.cmi
+nReference.cmo: nUri.cmi nReference.cmi
+nReference.cmx: nUri.cmx nReference.cmi
+nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi
+nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi
nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmx \
- nCicSubstitution.cmi
+ nCicSubstitution.cmi
nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \
- nCicSubstitution.cmi
-nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi
-nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
+ nCicSubstitution.cmi
+nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi
+nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmx nCicReduction.cmi
+ nCicEnvironment.cmi nCic.cmx nCicReduction.cmi
nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
+ nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \
- nCicTypeChecker.cmi
+ nCicTypeChecker.cmi
nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
- nCicTypeChecker.cmi
+ nCicTypeChecker.cmi
nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi
+ nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi
nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi
+ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi
nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
- nCicEnvironment.cmi nCic.cmx nCicPp.cmi
+ nCicEnvironment.cmi nCic.cmx nCicPp.cmi
nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
- nCicEnvironment.cmx nCic.cmx nCicPp.cmi
+ nCicEnvironment.cmx nCic.cmx nCicPp.cmi
-nCicLibrary.cmi:
-nCicLibrary.cmo: nCicLibrary.cmi
-nCicLibrary.cmx: nCicLibrary.cmi
+nCicLibrary.cmi:
+nCicLibrary.cmo: nCicLibrary.cmi
+nCicLibrary.cmx: nCicLibrary.cmi
-terms.cmi:
-pp.cmi: terms.cmi
-foSubst.cmi: terms.cmi
-orderings.cmi: terms.cmi
-foUtils.cmi: terms.cmi orderings.cmi
-foUnif.cmi: terms.cmi orderings.cmi
-index.cmi: terms.cmi orderings.cmi
-superposition.cmi: terms.cmi orderings.cmi index.cmi
-stats.cmi: terms.cmi orderings.cmi
-paramod.cmi: terms.cmi orderings.cmi
-nCicBlob.cmi: terms.cmi
-nCicProof.cmi: terms.cmi
-nCicParamod.cmi:
-terms.cmo: terms.cmi
-terms.cmx: terms.cmi
-pp.cmo: terms.cmi pp.cmi
-pp.cmx: terms.cmx pp.cmi
-foSubst.cmo: terms.cmi foSubst.cmi
-foSubst.cmx: terms.cmx foSubst.cmi
-orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi
-orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
-foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
-index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi
-index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi
+terms.cmi:
+pp.cmi: terms.cmi
+foSubst.cmi: terms.cmi
+orderings.cmi: terms.cmi
+foUtils.cmi: terms.cmi orderings.cmi
+foUnif.cmi: terms.cmi orderings.cmi
+index.cmi: terms.cmi orderings.cmi
+superposition.cmi: terms.cmi orderings.cmi index.cmi
+stats.cmi: terms.cmi orderings.cmi
+paramod.cmi: terms.cmi orderings.cmi
+nCicBlob.cmi: terms.cmi
+nCicProof.cmi: terms.cmi
+nCicParamod.cmi:
+terms.cmo: terms.cmi
+terms.cmx: terms.cmi
+pp.cmo: terms.cmi pp.cmi
+pp.cmx: terms.cmx pp.cmi
+foSubst.cmo: terms.cmi foSubst.cmi
+foSubst.cmx: terms.cmx foSubst.cmi
+orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi
+orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi
+foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
+foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
+foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
+foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
+index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi
+index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi
superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
- foUnif.cmi foSubst.cmi superposition.cmi
+ foUnif.cmi foSubst.cmi superposition.cmi
superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
- foUnif.cmx foSubst.cmx superposition.cmi
-stats.cmo: terms.cmi stats.cmi
-stats.cmx: terms.cmx stats.cmi
+ foUnif.cmx foSubst.cmx superposition.cmi
+stats.cmo: terms.cmi stats.cmi
+stats.cmx: terms.cmx stats.cmi
paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
- foUtils.cmi foUnif.cmi paramod.cmi
+ foUtils.cmi foUnif.cmi paramod.cmi
paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
- foUtils.cmx foUnif.cmx paramod.cmi
-nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi
-nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi
-nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi
-nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
+ foUtils.cmx foUnif.cmx paramod.cmi
+nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi
+nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi
+nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi
+nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
- nCicBlob.cmi nCicParamod.cmi
+ nCicBlob.cmi nCicParamod.cmi
nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
- nCicBlob.cmx nCicParamod.cmi
+ nCicBlob.cmx nCicParamod.cmi
-nDiscriminationTree.cmi:
-nCicMetaSubst.cmi:
-nCicUnifHint.cmi:
-nCicCoercion.cmi: nCicUnifHint.cmi
-nCicRefineUtil.cmi:
-nCicUnification.cmi: nCicCoercion.cmi
-nCicRefiner.cmi: nCicCoercion.cmi
-nDiscriminationTree.cmo: nDiscriminationTree.cmi
-nDiscriminationTree.cmx: nDiscriminationTree.cmi
-nCicMetaSubst.cmo: nCicMetaSubst.cmi
-nCicMetaSubst.cmx: nCicMetaSubst.cmi
-nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi
-nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi
+nDiscriminationTree.cmi:
+nCicMetaSubst.cmi:
+nCicUnifHint.cmi:
+nCicCoercion.cmi: nCicUnifHint.cmi
+nCicRefineUtil.cmi:
+nCicUnification.cmi: nCicCoercion.cmi
+nCicRefiner.cmi: nCicCoercion.cmi
+nDiscriminationTree.cmo: nDiscriminationTree.cmi
+nDiscriminationTree.cmx: nDiscriminationTree.cmi
+nCicMetaSubst.cmo: nCicMetaSubst.cmi
+nCicMetaSubst.cmx: nCicMetaSubst.cmi
+nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi
+nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi
nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi
+ nCicCoercion.cmi
nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmi
-nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi
-nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
-nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
+ nCicCoercion.cmi
+nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi
+nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi
+nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
+nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
nCicRefiner.cmo: nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
- nCicCoercion.cmi nCicRefiner.cmi
+ nCicCoercion.cmi nCicRefiner.cmi
nCicRefiner.cmx: nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
- nCicCoercion.cmx nCicRefiner.cmi
+ nCicCoercion.cmx nCicRefiner.cmi
-continuationals.cmi:
-nCicTacReduction.cmi:
-nTacStatus.cmi: continuationals.cmi
-nCicElim.cmi:
-nTactics.cmi: nTacStatus.cmi
-nnAuto.cmi: nTacStatus.cmi
-nDestructTac.cmi: nTacStatus.cmi
-nInversion.cmi: nTacStatus.cmi
-continuationals.cmo: continuationals.cmi
-continuationals.cmx: continuationals.cmi
-nCicTacReduction.cmo: nCicTacReduction.cmi
-nCicTacReduction.cmx: nCicTacReduction.cmi
-nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
-nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
-nCicElim.cmo: nCicElim.cmi
-nCicElim.cmx: nCicElim.cmi
-nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
-nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
+continuationals.cmi:
+nCicTacReduction.cmi:
+nTacStatus.cmi: continuationals.cmi
+nCicElim.cmi:
+nTactics.cmi: nTacStatus.cmi
+nnAuto.cmi: nTacStatus.cmi
+nDestructTac.cmi: nTacStatus.cmi
+nInversion.cmi: nTacStatus.cmi
+continuationals.cmo: continuationals.cmi
+continuationals.cmx: continuationals.cmi
+nCicTacReduction.cmo: nCicTacReduction.cmi
+nCicTacReduction.cmx: nCicTacReduction.cmi
+nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
+nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
+nCicElim.cmo: nCicElim.cmi
+nCicElim.cmx: nCicElim.cmi
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
+nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
nnAuto.cmo: nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
- continuationals.cmi nnAuto.cmi
+ continuationals.cmi nnAuto.cmi
nnAuto.cmx: nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
- continuationals.cmx nnAuto.cmi
+ continuationals.cmx nnAuto.cmi
nDestructTac.cmo: nTactics.cmi nTacStatus.cmi continuationals.cmi \
- nDestructTac.cmi
+ nDestructTac.cmi
nDestructTac.cmx: nTactics.cmx nTacStatus.cmx continuationals.cmx \
- nDestructTac.cmi
-nInversion.cmo: nTactics.cmi nCicElim.cmi continuationals.cmi nInversion.cmi
-nInversion.cmx: nTactics.cmx nCicElim.cmx continuationals.cmx nInversion.cmi
+ nDestructTac.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
-helm_registry.cmi:
-helm_registry.cmo: helm_registry.cmi
-helm_registry.cmx: helm_registry.cmi
+helm_registry.cmi:
+helm_registry.cmo: helm_registry.cmi
+helm_registry.cmx: helm_registry.cmi
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
-utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
-utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
+utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
+utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
-utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi
-utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
+utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
-threadSafe.cmi:
-extThread.cmi:
-threadSafe.cmo: threadSafe.cmi
-threadSafe.cmx: threadSafe.cmi
-extThread.cmo: extThread.cmi
-extThread.cmx: extThread.cmi
+threadSafe.cmi:
+extThread.cmi:
+threadSafe.cmo: threadSafe.cmi
+threadSafe.cmx: threadSafe.cmi
+extThread.cmo: extThread.cmi
+extThread.cmx: extThread.cmi
-xml.cmi:
-xmlPushParser.cmi:
-xml.cmo: xml.cmi
-xml.cmx: xml.cmi
-xmlPushParser.cmo: xmlPushParser.cmi
-xmlPushParser.cmx: xmlPushParser.cmi
+xml.cmi:
+xmlPushParser.cmi:
+xml.cmo: xml.cmi
+xml.cmx: xml.cmi
+xmlPushParser.cmo: xmlPushParser.cmi
+xmlPushParser.cmx: xmlPushParser.cmi
DEBUG_DEFAULT="true"
DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it"
RT_BASE_DIR_DEFAULT="`pwd`/matita"
-MATITA_VERSION="0.95.1"
+MATITA_VERSION="0.99.1"
DISTRIBUTED="yes" # "yes" for distributed tarballs
# End of distribution settings
-applyTransformation.cmo: applyTransformation.cmi
-applyTransformation.cmx: applyTransformation.cmi
-buildTimeConf.cmo:
-buildTimeConf.cmx:
+applyTransformation.cmo: applyTransformation.cmi
+applyTransformation.cmx: applyTransformation.cmi
+buildTimeConf.cmo:
+buildTimeConf.cmx:
cicMathView.cmo: matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
- buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi
+ buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi
cicMathView.cmx: matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
- buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi
-lablGraphviz.cmo: lablGraphviz.cmi
-lablGraphviz.cmx: lablGraphviz.cmi
-matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
-matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
-matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi
-matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx
-matitaEngine.cmo: matitaEngine.cmi
-matitaEngine.cmx: matitaEngine.cmi
-matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
-matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
-matitaGeneratedGui.cmo:
-matitaGeneratedGui.cmx:
+ buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi
+lablGraphviz.cmo: lablGraphviz.cmi
+lablGraphviz.cmx: lablGraphviz.cmi
+matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
+matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
+matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \
+ matitaEngine.cmi
+matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
+ matitaEngine.cmx
+matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
+matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
+matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
+matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
+matitaGeneratedGui.cmo:
+matitaGeneratedGui.cmx:
matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \
- matitaGtkMisc.cmi
+ matitaGtkMisc.cmi
matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
- matitaGtkMisc.cmi
+ matitaGtkMisc.cmi
matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmx \
- matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi
+ matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
+ matitaGeneratedGui.cmx matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi
matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
- matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \
- matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
-matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi
-matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
+ matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
+ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
+matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi
+matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
- matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \
- cicMathView.cmi buildTimeConf.cmx applyTransformation.cmi \
- matitaMathView.cmi
+ matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmx \
+ matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmx \
+ applyTransformation.cmi matitaMathView.cmi
matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
- matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \
- cicMathView.cmx buildTimeConf.cmx applyTransformation.cmx \
- matitaMathView.cmi
-matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
-matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
+ matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \
+ matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \
+ applyTransformation.cmx matitaMathView.cmi
+matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
+matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \
- matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmx
+ matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmx applyTransformation.cmi
matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaInit.cmx \
- matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx
+ matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx applyTransformation.cmx
matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \
- buildTimeConf.cmx matitaScript.cmi
+ buildTimeConf.cmx matitaScript.cmi
matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \
- buildTimeConf.cmx matitaScript.cmi
-matitaTypes.cmo: matitaTypes.cmi
-matitaTypes.cmx: matitaTypes.cmi
-predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi
-predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi
-virtuals.cmo: virtuals.cmi
-virtuals.cmx: virtuals.cmi
-applyTransformation.cmi:
-cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi
-lablGraphviz.cmi:
-matitaclean.cmi:
-matitaEngine.cmi:
-matitaExcPp.cmi:
-matitaGtkMisc.cmi: matitaGeneratedGui.cmx
-matitaGui.cmi: matitaGuiTypes.cmi
-matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx \
- applyTransformation.cmi
-matitaInit.cmi:
-matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
-matitaMisc.cmi: matitaGuiTypes.cmi
-matitaScript.cmi:
-matitaTypes.cmi:
-predefined_virtuals.cmi:
-virtuals.cmi:
+ buildTimeConf.cmx matitaScript.cmi
+matitaTypes.cmo: matitaTypes.cmi
+matitaTypes.cmx: matitaTypes.cmi
+predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi
+predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi
+virtuals.cmo: virtuals.cmi
+virtuals.cmx: virtuals.cmi
+applyTransformation.cmi:
+cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi
+lablGraphviz.cmi:
+matitaclean.cmi:
+matitaEngine.cmi: applyTransformation.cmi
+matitaExcPp.cmi:
+matitaGtkMisc.cmi: matitaGeneratedGui.cmx
+matitaGui.cmi: matitaGuiTypes.cmi
+matitaGuiTypes.cmi: matitaGeneratedGui.cmx applyTransformation.cmi
+matitaInit.cmi:
+matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
+matitaMisc.cmi: matitaGuiTypes.cmi
+matitaScript.cmi:
+matitaTypes.cmi:
+predefined_virtuals.cmi:
+virtuals.cmi:
-0.95.1 - 17/11/2011 - alpha version for the 1.x series
+0.99.1 - 17/11/2011 - alpha version for the 1.x series
* old kernel, unification, etc. removed
* new compact syntax for tactics
* improved automation
op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i))
\big[op,nil]_{i ∈ [a,b[ |p i}(f i).
#a #b # c #p #B #nil #op #f #leab #lebc
->(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?) /2/
+>(plus_minus_m_m (c-a) (b-a)) {⊢ (??%?)} /2/
>minus_plus >(commutative_plus a) <plus_minus_m_m //
>bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
[#i #lei >plus_minus // <plus_minus1
#n #Hind cases(true_or_false (p1 n)) #Hp1
[>bigop_Strue // >Hind >bigop_sum @same_bigop
#i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
- #eqi [|#H] (>eqi in ⊢ (???%))
+ #eqi [|#H] >eqi {⊢ (???%)}
>div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize //
|>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
#i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
- #eqi >eqi in ⊢ (???%) >div_plus_times /2/
+ #eqi >eqi {⊢ (???%)} >div_plus_times /2/
]
qed.
#k #p #B #nil #op #f #g (elim k) [normalize @nill]
-k #k #Hind (cases (true_or_false (p k))) #H
[>bigop_Strue // >bigop_Strue // >bigop_Strue //
- normalize <assoc <assoc in ⊢ (???%) @eq_f >assoc >comm in ⊢ (??(????%?)?)
+ normalize <assoc <assoc {⊢ (???%)} @eq_f >assoc >comm {⊢ (??(????%?)?)}
<assoc @eq_f @Hind
|>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
]
iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
\big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
#n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
-@(le_gen ? n1) #i (generalize in match p2) (elim i)
+@(le_gen ? n1) #i generalize {match p2} (elim i)
[(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
>bigop_Sfalse
[@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
|#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) *
#ltkj #p1kj #eqj % // % //
(cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
- #eqkj @False_ind generalize in match p2j @eqb_elim
+ #eqkj @False_ind generalize {match p2j} @eqb_elim
normalize /2/
]
|>bigop_Sfalse // @(Hind ? len)
record Dop (A:Type[0]) (nil:A): Type[0] ≝
{sum : ACop A nil;
prod: A → A →A;
- null: \forall a. prod a nil = nil;
+ null: ∀a. prod a nil = nil;
distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
}.
-theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.\forall f,a.
- let aop \def sum B nil R in
- let mop \def prod B nil R in
+theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.∀f,a.
+ let aop ≝ sum B nil R in
+ let mop ≝ prod B nil R in
mop a \big[aop,nil]_{i<n|p i}(f i) =
\big[aop,nil]_{i<n|p i}(mop a (f i)).
#n #p #B #nil #R #f #a normalize (elim n) [@null]
cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc
lapply (Hind c (le_S_S_to_le … lec)) #Hc
lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
- >(plus_minus_m_m m c) in ⊢ (??(??(?%))) [|@le_S_S_to_le //]
+ >(plus_minus_m_m m c) {⊢ (??(??(?%)))} [|@le_S_S_to_le //]
>commutative_plus >(distributive_times_plus ? (S c))
@divides_plus
[>associative_times >(commutative_times (S c))
<associative_times @divides_times //
- |<(fact_minus …ltcm) in ⊢ (?(??%)?)
+ |<(fact_minus …ltcm) {⊢ (?(??%)?)}
<associative_times @divides_times //
>commutative_times @Hmc
]
theorem bc1: ∀n.∀k. k < n →
bc (S n) (S k) = (bc n k) + (bc n (S k)).
#n #k #ltkn > bceq >(bceq n) >(bceq n (S k))
->(div_times_times ?? (S k)) in ⊢ (???(?%?))
+>(div_times_times ?? (S k)) {⊢ (???(?%?))}
[|>(times_n_O 0) @lt_times // | //]
->associative_times in ⊢ (???(?(??%)?))
->commutative_times in ⊢ (???(?(??(??%))?))
-<associative_times in ⊢ (???(?(??%)?))
->(div_times_times ?? (n - k)) in ⊢ (???(??%))
+>associative_times {⊢ (???(?(??%)?))}
+>commutative_times {⊢ (???(?(??(??%))?))}
+<associative_times {⊢ (???(?(??%)?))}
+>(div_times_times ?? (n - k)) {⊢ (???(??%))}
[|>(times_n_O 0) @lt_times //
|@(le_plus_to_le_r k ??) <plus_minus_m_m /2/]
->associative_times in ⊢ (???(??(??%)))
+>associative_times {⊢ (???(??(??%)))}
>fact_minus // <plus_div
[<distributive_times_plus
- >commutative_plus
in ⊢ (???%) <plus_n_Sm <plus_minus_m_m [|/2/] @refl
+ >commutative_plus
{⊢ (???%)} <plus_n_Sm <plus_minus_m_m [|/2/] @refl
|<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
|>associative_times >(commutative_times (S k))
<associative_times @divides_times // @bc2 /2/
<commutative_plus <plus_minus
[@(eq_times_plus_to_congruent … posm) //
|applyS monotonic_le_times_r @(transitive_le ? ((a+b*m)*d)) //
- applyS monotonic_le_times_r apply (transitive_le … (b*m)) /2/
+ applyS monotonic_le_times_r @(transitive_le … (b*m)) /2/
]
|(* congruent to b *)
-pnm (cut (d*m = c*n-1))
#m #n #a #b #ltam #ltbn #pnm
cut (andb (eqb ((cr_pair m n a b) \mod m) a)
(eqb ((cr_pair m n a b) \mod n) b) = true)
- [whd in match (cr_pair m n a b) @f_min_true cases(congruent_ab_lt m n a b ?? pnm)
+ [whd {match (cr_pair m n a b)} @f_min_true cases(congruent_ab_lt m n a b ?? pnm)
[#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/
>eq_to_eqb_true
[>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) //
qed.
theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
-#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?)
+#n #p #posp >(div_mod (n \mod p) p) {⊢ (? ? % ?) }
>(eq_div_O ? p) // @lt_mod_m_m //
qed.
theorem congruent_to_divides: ∀n,m,p:nat.O < p →
n ≅_{p} m → p ∣ (n - m).
#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
->commutative_times >(div_mod n p) in ⊢ (??%?)
->(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
+>commutative_times >(div_mod n p) {⊢ (??%?)}
+>(div_mod m p) {⊢ (??%?)} <(commutative_plus (m \mod p))
<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
qed.
#n #q #posq
(elim (le_to_or_lt_eq ?? (lt_mod_m_m n q posq))) #H
[%2 % // applyS eq_f //
- |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)) @eq_f//
+ |%1 % // /demod/ <H {⊢(? ? ? (? % ?))} @eq_f//
]
qed.
theorem lt_div_S: ∀n,m. O < m → n < S(n / m)*m.
#n #m #posm (change with (n < m +(n/m)*m))
->(div_mod n m) in ⊢ (? % ?) >commutative_plus
+>(div_mod n m) {⊢ (? % ?)} >commutative_plus
@monotonic_lt_plus_l @lt_mod_m_m //
qed.
theorem le_div: ∀n,m. O < n → m/n ≤ m.
#n #m #posn
->(div_mod m n) in ⊢ (? ? %) @(transitive_le ? (m/n*n)) /2/
+>(div_mod m n) {⊢ (? ? %)} @(transitive_le ? (m/n*n)) /2/
qed.
theorem le_plus_mod: ∀m,n,q. O < q →
@(div_mod_spec_to_eq2 … (m/q + n/q) ? (div_mod_spec_div_mod … posq)).
@div_mod_spec_intro
[@not_le_to_lt //
- |>(div_mod n q) in ⊢ (? ? (? ? %) ?)
+ |>(div_mod n q) {⊢ (? ? (? ? %) ?)}
(applyS (eq_f … (λx.plus x (n \mod q))))
- >(div_mod m q) in ⊢ (? ? (? % ?) ?)
+ >(div_mod m q) {⊢ (? ? (? % ?) ?)}
(applyS (eq_f … (λx.plus x (m \mod q)))) //
]
]
#m #n #q #posq @(le_times_to_le … posq)
@(le_plus_to_le_r ((m+n) \mod q))
(* bruttino *)
->commutative_times
in ⊢ (? ? %) <div_mod
->(div_mod m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %))
->commutative_plus in ⊢ (? ? (? % ?)) >associative_plus in ⊢ (? ? %)
-<associative_plus in ⊢ (? ? (? ? %)) (applyS monotonic_le_plus_l) /2/
+>commutative_times
{⊢ (? ? %)} <div_mod
+>(div_mod m q) {⊢ (? ? (? % ?))} >(div_mod n q) {⊢ (? ? (? ? %))}
+>commutative_plus {⊢ (? ? (? % ?))} >associative_plus {⊢ (? ? %)}
+<associative_plus {⊢ (? ? (? ? %))} (applyS monotonic_le_plus_l) /2/
qed.
theorem le_times_to_le_div: ∀a,b,c:nat.
#b #lt1b @nat_elim2 normalize
[#n #H @sym_eq @(exp_to_eq_O b n lt1b) //
|#n #H @False_ind @(absurd (1 < 1) ? (not_le_Sn_n 1))
- <H in ⊢ (??%) @(lt_to_le_to_lt ? (1*b)) //
+ <H {⊢ (??%)} @(lt_to_le_to_lt ? (1*b)) //
@le_times // @lt_O_exp /2/
|#n #m #Hind #H @eq_f @Hind @(injective_times_l … H) /2/
]
@(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n))))
[@le_times[@le_times //]//
(* we generalize to hide the computational content *)
- |normalize in match ((S n)!) generalize in match (S n)
- #Sn generalize in match 2 #two //
+ |normalize {match ((S n)!)} generalize {match (S n)}
+ #Sn generalize {match 2} #two //
]
]
qed.
#n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H
cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1
@(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n))))
- [normalize in match ((S n)!) generalize in match (S n) #Sn
- generalize in match 2 #two //
+ [normalize {match ((S n)!)} generalize {match (S n)} #Sn
+ generalize {match 2} #two //
|cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n)))))
[>H //] #H2 >H2 @lt_to_le_to_lt_times
[@lt_to_le_to_lt_times //|>H // | //]
lemma divides_to_gcd_aux: ∀p,m,n. O < p → O < n →n ∣ m →
gcd_aux p m n = n.
-#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm whd in ⊢ (??%?)
+#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm whd {⊢ (??%?)}
>divides_to_dividesb_true normalize //
qed.
lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m →
gcd_aux (S p) m n = gcd_aux p n (m \mod n).
-#p #m #n #lenm #divnm whd in ⊢ (??%?) >not_divides_to_dividesb_false
+#p #m #n #lenm #divnm whd {⊢ (??%?)} >not_divides_to_dividesb_false
normalize // qed.
theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p →
[(* first case *)
<H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %2
<commutative_plus >distributive_times_plus_r
- >(div_mod m n) in ⊢(? ? (? % ?) ?)
+ >(div_mod m n) {⊢(? ? (? % ?) ?)}
>associative_times <commutative_plus >distributive_times_plus
<minus_plus <commutative_plus <plus_minus //
|(* second case *)
<H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
>distributive_times_plus_r
- >(div_mod m n) in ⊢ (? ? (? ? %) ?)
+ >(div_mod m n) {⊢ (? ? (? ? %) ?)}
>distributive_times_plus >associative_times
<minus_plus <commutative_plus <plus_minus //
]
theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
gcd p n = 1 → p ∣ (n*m) → p ∣ m.
#p #m #n #posn #gcd1 * #c #nm
-cases(eq_minus_gcd m p) #a * #b * #H >gcd1 in H #H
+cases(eq_minus_gcd m p) #a * #b * #H >gcd1 {H} #H
[@(quotient ?? (a*n-c*b)) >distributive_times_minus <associative_times
<associative_times <nm >(commutative_times m) >commutative_times
>associative_times <distributive_times_minus //
theorem divides_to_divides_times: ∀p,q,n. prime p → p ∤ q →
p ∣ n → q ∣ n → p*q ∣ n.
-#p #q #n #primep #notdivpq #divpn * #b #eqn (>eqn in divpn)
+#p #q #n #primep #notdivpq #divpn * #b #eqn (>eqn {divpn})
#divpn cases(divides_times_to_divides ??? primep divpn) #H
[@False_ind /2/
|cases H #c #eqb @(quotient ?? c) >eqb <associative_times //
theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
#f #n #posn @(lt_O_n_elim ? posn) #m
-normalize (cases (f m)) normalize apply le_S_S //
+normalize (cases (f m)) normalize @le_S_S //
@le_max_n qed.
theorem le_to_le_max : ∀f.∀n,m.
theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) →
max n f = max n g.
#f #g #n (elim n) //
-#m #Hind #ext normalize >ext normalize in Hind >Hind //
+#m #Hind #ext normalize >ext normalize {Hind} >Hind //
#i #ltim @ext /2/
qed.
(let previous_prime ≝ (nth_prime n) in
let upper_bound ≝ S previous_prime! in
S previous_prime ≤ min upper_bound (S previous_prime) primeb)
-apply le_min_l
+@le_min_l
qed.
theorem lt_SO_nth_prime_n : ∀n:nat. 1 < nth_prime n.
lemma gral: ∀A.∀x,y:A.
mk_Sigma A x = mk_Sigma A y → x=y.
#A #x #y #E lapply (tech1 ?? E)
- generalize in ⊢ (??(???%?)? → ?) #E1
- normalize in E1; >(K ?? E1) normalize
+ generalize {⊢ (??(???%?)? → ?)} #E1
+ normalize {E1}; >(K ?? E1) normalize
#H @H
qed.
lemma jm_to_eq_sigma:
∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
- #A #x #y #E cases E in ⊢ (???%); %
+ #A #x #y #E cases E {⊢ (???%)} %
qed.
definition curry:
lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
P y h.
- #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
+ #A #x #P #H #y #E lapply (gral ??? E) #G generalize {match E}
@(match G
return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
with
#A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
lapply (G ?? (curry ?? P) ?? F)
[ normalize //
- | #H whd in H; @(H : PP ? (P b) ?) ]
+ | #H whd {H} @(H : PP ? (P b) ?) ]
qed.
lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
lemma eq_rect_Type0_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
cases p; //; qed.
lemma eq_rect_Type1_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
cases p; //; qed.
lemma eq_rect_Type2_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
cases p; //; qed.
lemma eq_rect_Type3_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
cases p; //; qed.
theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
let clean_current_baseuri status =
LibraryClean.clean_baseuris [status#baseuri]
-let save_moo status =
- let script = MatitaScript.current () in
+let save_moo0 ~do_clean script status =
let baseuri = status#baseuri in
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
status
- | _ -> clean_current_baseuri status
+ | _ -> if do_clean then clean_current_baseuri status
+;;
+
+let save_moo status =
+ let script = MatitaScript.current () in
+ save_moo0 ~do_clean:true script status
;;
let ask_unsaved parent filename =
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
+ val mutable current_page = 0
initializer
let s () = MatitaScript.current () in
MatitaMisc.reset_font_size;
ignore (main#scriptNotebook#connect#switch_page
(fun page ->
+ let old_script = MatitaScript.at_page current_page in
+ save_moo0 ~do_clean:false old_script old_script#status;
+ current_page <- page;
let script = MatitaScript.at_page page in
script#activate;
main#saveMenuItem#misc#set_sensitive script#has_name))
projects / helm.git / commitdiff