From ddc80515997a3f56085c6234d4db326141e189aa Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2011 13:07:03 +0000 Subject: [PATCH] * Almost ready for release 0.99.1. * Syntax changed: *H => * as H -H1 .. HN => -H1 .. -HN intros => ## pattern: in ... => {...} * Library ported to the new syntax --- matita/components/content/.depend.opt | 28 ++-- matita/components/content_pres/.depend.opt | 60 ++++----- matita/components/disambiguation/.depend.opt | 18 +-- matita/components/extlib/.depend.opt | 54 ++++---- matita/components/getter/.depend.opt | 52 ++++---- matita/components/grafite/.depend.opt | 10 +- matita/components/grafite_engine/.depend.opt | 18 +-- matita/components/grafite_parser/.depend.opt | 15 +-- .../grafite_parser/grafiteParser.ml | 41 ++---- matita/components/library/.depend.opt | 18 +-- matita/components/logger/.depend.opt | 6 +- matita/components/ng_cic_content/.depend.opt | 12 +- .../components/ng_disambiguation/.depend.opt | 24 ++-- matita/components/ng_kernel/.depend.opt | 58 ++++----- matita/components/ng_library/.depend.opt | 6 +- .../components/ng_paramodulation/.depend.opt | 78 +++++------ matita/components/ng_refiner/.depend.opt | 42 +++--- matita/components/ng_tactics/.depend.opt | 50 +++---- matita/components/registry/.depend.opt | 6 +- matita/components/syntax_extensions/.depend | 10 +- .../components/syntax_extensions/.depend.opt | 10 +- matita/components/thread/.depend.opt | 12 +- matita/components/xml/.depend.opt | 12 +- matita/configure.ac | 2 +- matita/matita/.depend.opt | 123 +++++++++--------- matita/matita/dist/ChangeLog | 2 +- matita/matita/lib/arithmetics/bigops.ma | 20 +-- matita/matita/lib/arithmetics/binomial.ma | 18 +-- .../lib/arithmetics/chinese_reminder.ma | 4 +- matita/matita/lib/arithmetics/congruence.ma | 6 +- matita/matita/lib/arithmetics/div_and_mod.ma | 18 +-- matita/matita/lib/arithmetics/exp.ma | 2 +- matita/matita/lib/arithmetics/factorial.ma | 8 +- matita/matita/lib/arithmetics/gcd.ma | 12 +- matita/matita/lib/arithmetics/minimization.ma | 4 +- matita/matita/lib/arithmetics/primes.ma | 2 +- matita/matita/lib/basics/jmeq.ma | 10 +- matita/matita/lib/basics/logic.ma | 8 +- matita/matita/matitaGui.ml | 14 +- 39 files changed, 439 insertions(+), 454 deletions(-) diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index 34a327264..aec750131 100644 --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -1,14 +1,14 @@ -content.cmi: -notationUtil.cmi: notationPt.cmx -notationEnv.cmi: notationPt.cmx -notationPp.cmi: notationPt.cmx notationEnv.cmi -notationPt.cmo: -notationPt.cmx: -content.cmo: content.cmi -content.cmx: content.cmi -notationUtil.cmo: notationPt.cmx notationUtil.cmi -notationUtil.cmx: notationPt.cmx notationUtil.cmi -notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi -notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi -notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi -notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi +content.cmi: +notationUtil.cmi: notationPt.cmx +notationEnv.cmi: notationPt.cmx +notationPp.cmi: notationPt.cmx notationEnv.cmi +notationPt.cmo: +notationPt.cmx: +content.cmo: content.cmi +content.cmx: content.cmi +notationUtil.cmo: notationPt.cmx notationUtil.cmi +notationUtil.cmx: notationPt.cmx notationUtil.cmi +notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi +notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi +notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi +notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi diff --git a/matita/components/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt index 5c11c1ded..03a1732eb 100644 --- a/matita/components/content_pres/.depend.opt +++ b/matita/components/content_pres/.depend.opt @@ -1,38 +1,38 @@ -renderingAttrs.cmi: -cicNotationLexer.cmi: -cicNotationParser.cmi: -mpresentation.cmi: -box.cmi: -content2presMatcher.cmi: -termContentPres.cmi: cicNotationParser.cmi -boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi -cicNotationPres.cmi: mpresentation.cmi box.cmi -content2pres.cmi: termContentPres.cmi cicNotationPres.cmi -renderingAttrs.cmo: renderingAttrs.cmi -renderingAttrs.cmx: renderingAttrs.cmi -cicNotationLexer.cmo: cicNotationLexer.cmi -cicNotationLexer.cmx: cicNotationLexer.cmi -cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi -cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi -mpresentation.cmo: mpresentation.cmi -mpresentation.cmx: mpresentation.cmi -box.cmo: renderingAttrs.cmi box.cmi -box.cmx: renderingAttrs.cmx box.cmi -content2presMatcher.cmo: content2presMatcher.cmi -content2presMatcher.cmx: content2presMatcher.cmi +renderingAttrs.cmi: +cicNotationLexer.cmi: +cicNotationParser.cmi: +mpresentation.cmi: +box.cmi: +content2presMatcher.cmi: +termContentPres.cmi: cicNotationParser.cmi +boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi +cicNotationPres.cmi: mpresentation.cmi box.cmi +content2pres.cmi: termContentPres.cmi cicNotationPres.cmi +renderingAttrs.cmo: renderingAttrs.cmi +renderingAttrs.cmx: renderingAttrs.cmi +cicNotationLexer.cmo: cicNotationLexer.cmi +cicNotationLexer.cmx: cicNotationLexer.cmi +cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi +cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi +mpresentation.cmo: mpresentation.cmi +mpresentation.cmx: mpresentation.cmi +box.cmo: renderingAttrs.cmi box.cmi +box.cmx: renderingAttrs.cmx box.cmi +content2presMatcher.cmo: content2presMatcher.cmi +content2presMatcher.cmx: content2presMatcher.cmi termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \ - cicNotationParser.cmi termContentPres.cmi + cicNotationParser.cmi termContentPres.cmi termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi + cicNotationParser.cmx termContentPres.cmi boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ - boxPp.cmi + boxPp.cmi boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ - boxPp.cmi + boxPp.cmi cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \ - cicNotationPres.cmi + cicNotationPres.cmi cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \ - cicNotationPres.cmi + cicNotationPres.cmi content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ - cicNotationPres.cmi box.cmi content2pres.cmi + cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ - cicNotationPres.cmx box.cmx content2pres.cmi + cicNotationPres.cmx box.cmx content2pres.cmi diff --git a/matita/components/disambiguation/.depend.opt b/matita/components/disambiguation/.depend.opt index 9fdbeeeaf..fa6388aa7 100644 --- a/matita/components/disambiguation/.depend.opt +++ b/matita/components/disambiguation/.depend.opt @@ -1,11 +1,11 @@ -disambiguateTypes.cmi: -disambiguate.cmi: disambiguateTypes.cmi -multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi -disambiguateTypes.cmo: disambiguateTypes.cmi -disambiguateTypes.cmx: disambiguateTypes.cmi -disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi -disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi +disambiguateTypes.cmi: +disambiguate.cmi: disambiguateTypes.cmi +multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi +disambiguateTypes.cmo: disambiguateTypes.cmi +disambiguateTypes.cmx: disambiguateTypes.cmi +disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi +disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \ - multiPassDisambiguator.cmi + multiPassDisambiguator.cmi multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \ - multiPassDisambiguator.cmi + multiPassDisambiguator.cmi diff --git a/matita/components/extlib/.depend.opt b/matita/components/extlib/.depend.opt index f6168c1bc..b121fbcd1 100644 --- a/matita/components/extlib/.depend.opt +++ b/matita/components/extlib/.depend.opt @@ -1,27 +1,27 @@ -componentsConf.cmi: -hExtlib.cmi: -hMarshal.cmi: -patternMatcher.cmi: -hLog.cmi: -trie.cmi: -discrimination_tree.cmi: -hTopoSort.cmi: -graphvizPp.cmi: -componentsConf.cmo: componentsConf.cmi -componentsConf.cmx: componentsConf.cmi -hExtlib.cmo: hExtlib.cmi -hExtlib.cmx: hExtlib.cmi -hMarshal.cmo: hExtlib.cmi hMarshal.cmi -hMarshal.cmx: hExtlib.cmx hMarshal.cmi -patternMatcher.cmo: patternMatcher.cmi -patternMatcher.cmx: patternMatcher.cmi -hLog.cmo: hLog.cmi -hLog.cmx: hLog.cmi -trie.cmo: trie.cmi -trie.cmx: trie.cmi -discrimination_tree.cmo: trie.cmi 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 diff --git a/matita/components/getter/.depend.opt b/matita/components/getter/.depend.opt index 64da37f13..301b9d8b8 100644 --- a/matita/components/getter/.depend.opt +++ b/matita/components/getter/.depend.opt @@ -1,38 +1,38 @@ -http_getter_wget.cmi: -http_getter_logger.cmi: -http_getter_misc.cmi: -http_getter_const.cmi: -http_getter_env.cmi: http_getter_types.cmx -http_getter_storage.cmi: -http_getter_common.cmi: http_getter_types.cmx -http_getter.cmi: http_getter_types.cmx -http_getter_types.cmo: -http_getter_types.cmx: -http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi -http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi -http_getter_logger.cmo: http_getter_logger.cmi -http_getter_logger.cmx: http_getter_logger.cmi -http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi -http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi -http_getter_const.cmo: http_getter_const.cmi -http_getter_const.cmx: http_getter_const.cmi +http_getter_wget.cmi: +http_getter_logger.cmi: +http_getter_misc.cmi: +http_getter_const.cmi: +http_getter_env.cmi: http_getter_types.cmx +http_getter_storage.cmi: +http_getter_common.cmi: http_getter_types.cmx +http_getter.cmi: http_getter_types.cmx +http_getter_types.cmo: +http_getter_types.cmx: +http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi +http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi +http_getter_logger.cmo: http_getter_logger.cmi +http_getter_logger.cmx: http_getter_logger.cmi +http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi +http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi +http_getter_const.cmo: http_getter_const.cmi +http_getter_const.cmx: http_getter_const.cmi http_getter_env.cmo: http_getter_types.cmx http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi + http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi http_getter_env.cmx: http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi + http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi http_getter_storage.cmo: http_getter_wget.cmi http_getter_types.cmx \ - http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi + http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi http_getter_storage.cmx: http_getter_wget.cmx http_getter_types.cmx \ - http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi + http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi http_getter_common.cmo: http_getter_types.cmx http_getter_misc.cmi \ - http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi + http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi http_getter_common.cmx: http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi + http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi http_getter.cmo: http_getter_wget.cmi http_getter_types.cmx \ http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ - http_getter.cmi + http_getter.cmi http_getter.cmx: http_getter_wget.cmx http_getter_types.cmx \ http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ - http_getter.cmi + http_getter.cmi diff --git a/matita/components/grafite/.depend.opt b/matita/components/grafite/.depend.opt index 3a2590d84..fbe333cbd 100644 --- a/matita/components/grafite/.depend.opt +++ b/matita/components/grafite/.depend.opt @@ -1,5 +1,5 @@ -grafiteAstPp.cmi: grafiteAst.cmx -grafiteAst.cmo: -grafiteAst.cmx: -grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi -grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi +grafiteAstPp.cmi: grafiteAst.cmx +grafiteAst.cmo: +grafiteAst.cmx: +grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi +grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi diff --git a/matita/components/grafite_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt index d04ec9d2c..27787b008 100644 --- a/matita/components/grafite_engine/.depend.opt +++ b/matita/components/grafite_engine/.depend.opt @@ -1,11 +1,11 @@ -grafiteTypes.cmi: -nCicCoercDeclaration.cmi: grafiteTypes.cmi -grafiteEngine.cmi: grafiteTypes.cmi -grafiteTypes.cmo: grafiteTypes.cmi -grafiteTypes.cmx: grafiteTypes.cmi -nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi -nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi +grafiteTypes.cmi: +nCicCoercDeclaration.cmi: grafiteTypes.cmi +grafiteEngine.cmi: grafiteTypes.cmi +grafiteTypes.cmo: grafiteTypes.cmi +grafiteTypes.cmx: grafiteTypes.cmi +nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi +nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \ - grafiteEngine.cmi + grafiteEngine.cmi grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \ - grafiteEngine.cmi + grafiteEngine.cmi diff --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index b8b65a8c0..5142da1bf 100644 --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@ -1,9 +1,6 @@ -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 diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 9e1e54ee7..37569bea6 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -101,12 +101,6 @@ EXTEND 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 ] @@ -115,7 +109,6 @@ EXTEND [ 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] @@ -138,14 +131,15 @@ EXTEND ]; 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 @@ -178,19 +172,8 @@ EXTEND | 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 [ @@ -202,8 +185,6 @@ EXTEND SYMBOL <:unicode>; 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 @@ -221,22 +202,20 @@ EXTEND | 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 @@ -255,8 +234,6 @@ EXTEND 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)]) @@ -272,7 +249,7 @@ EXTEND | 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: [ diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt index 975c9e8da..28703386a 100644 --- a/matita/components/library/.depend.opt +++ b/matita/components/library/.depend.opt @@ -1,9 +1,9 @@ -librarian.cmi: -libraryMisc.cmi: -libraryClean.cmi: -librarian.cmo: librarian.cmi -librarian.cmx: librarian.cmi -libraryMisc.cmo: libraryMisc.cmi -libraryMisc.cmx: libraryMisc.cmi -libraryClean.cmo: 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 diff --git a/matita/components/logger/.depend.opt b/matita/components/logger/.depend.opt index dfb4400ff..1c8ec5b7c 100644 --- a/matita/components/logger/.depend.opt +++ b/matita/components/logger/.depend.opt @@ -1,3 +1,3 @@ -helmLogger.cmi: -helmLogger.cmo: helmLogger.cmi -helmLogger.cmx: helmLogger.cmi +helmLogger.cmi: +helmLogger.cmo: helmLogger.cmi +helmLogger.cmx: helmLogger.cmi diff --git a/matita/components/ng_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt index fd1b831b9..b1a499fd3 100644 --- a/matita/components/ng_cic_content/.depend.opt +++ b/matita/components/ng_cic_content/.depend.opt @@ -1,6 +1,6 @@ -ncic2astMatcher.cmi: -interpretations.cmi: -ncic2astMatcher.cmo: ncic2astMatcher.cmi -ncic2astMatcher.cmx: ncic2astMatcher.cmi -interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi -interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi +ncic2astMatcher.cmi: +interpretations.cmi: +ncic2astMatcher.cmo: ncic2astMatcher.cmi +ncic2astMatcher.cmx: ncic2astMatcher.cmi +interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi +interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi diff --git a/matita/components/ng_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt index 0810bc8be..d5306074a 100644 --- a/matita/components/ng_disambiguation/.depend.opt +++ b/matita/components/ng_disambiguation/.depend.opt @@ -1,14 +1,14 @@ -nnumber_notation.cmi: -disambiguateChoices.cmi: -nCicDisambiguate.cmi: -grafiteDisambiguate.cmi: -nnumber_notation.cmo: nnumber_notation.cmi -nnumber_notation.cmx: nnumber_notation.cmi -disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi -disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi -nCicDisambiguate.cmo: nCicDisambiguate.cmi -nCicDisambiguate.cmx: nCicDisambiguate.cmi +nnumber_notation.cmi: +disambiguateChoices.cmi: +nCicDisambiguate.cmi: +grafiteDisambiguate.cmi: +nnumber_notation.cmo: nnumber_notation.cmi +nnumber_notation.cmx: nnumber_notation.cmi +disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi +disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi +nCicDisambiguate.cmo: nCicDisambiguate.cmi +nCicDisambiguate.cmx: nCicDisambiguate.cmi grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \ - grafiteDisambiguate.cmi + grafiteDisambiguate.cmi grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \ - grafiteDisambiguate.cmi + grafiteDisambiguate.cmi diff --git a/matita/components/ng_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt index 5e4dabb6a..c57bf8efe 100644 --- a/matita/components/ng_kernel/.depend.opt +++ b/matita/components/ng_kernel/.depend.opt @@ -1,41 +1,41 @@ -nUri.cmi: -nReference.cmi: nUri.cmi -nCicUtils.cmi: nCic.cmx -nCicSubstitution.cmi: nCic.cmx -nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx -nCicReduction.cmi: nCic.cmx -nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx -nCicUntrusted.cmi: nCic.cmx -nCicPp.cmi: nReference.cmi nCic.cmx -nCic.cmo: nUri.cmi nReference.cmi -nCic.cmx: nUri.cmx nReference.cmx -nUri.cmo: nUri.cmi -nUri.cmx: nUri.cmi -nReference.cmo: nUri.cmi nReference.cmi -nReference.cmx: nUri.cmx nReference.cmi -nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi -nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi +nUri.cmi: +nReference.cmi: nUri.cmi +nCicUtils.cmi: nCic.cmx +nCicSubstitution.cmi: nCic.cmx +nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx +nCicReduction.cmi: nCic.cmx +nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx +nCicUntrusted.cmi: nCic.cmx +nCicPp.cmi: nReference.cmi nCic.cmx +nCic.cmo: nUri.cmi nReference.cmi +nCic.cmx: nUri.cmx nReference.cmx +nUri.cmo: nUri.cmi +nUri.cmx: nUri.cmi +nReference.cmo: nUri.cmi nReference.cmi +nReference.cmx: nUri.cmx nReference.cmi +nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi +nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmx \ - nCicSubstitution.cmi + nCicSubstitution.cmi nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \ - nCicSubstitution.cmi -nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi -nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi + nCicSubstitution.cmi +nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi +nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicEnvironment.cmi nCic.cmx nCicReduction.cmi + nCicEnvironment.cmi nCic.cmx nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi + nCicEnvironment.cmx nCic.cmx nCicReduction.cmi nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \ - nCicTypeChecker.cmi + nCicTypeChecker.cmi nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ - nCicTypeChecker.cmi + nCicTypeChecker.cmi nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi + nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi + nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ - nCicEnvironment.cmi nCic.cmx nCicPp.cmi + nCicEnvironment.cmi nCic.cmx nCicPp.cmi nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi + nCicEnvironment.cmx nCic.cmx nCicPp.cmi diff --git a/matita/components/ng_library/.depend.opt b/matita/components/ng_library/.depend.opt index 48127a325..b9e7731f9 100644 --- a/matita/components/ng_library/.depend.opt +++ b/matita/components/ng_library/.depend.opt @@ -1,3 +1,3 @@ -nCicLibrary.cmi: -nCicLibrary.cmo: nCicLibrary.cmi -nCicLibrary.cmx: nCicLibrary.cmi +nCicLibrary.cmi: +nCicLibrary.cmo: nCicLibrary.cmi +nCicLibrary.cmx: nCicLibrary.cmi diff --git a/matita/components/ng_paramodulation/.depend.opt b/matita/components/ng_paramodulation/.depend.opt index 2e31be0ec..f6eae06d6 100644 --- a/matita/components/ng_paramodulation/.depend.opt +++ b/matita/components/ng_paramodulation/.depend.opt @@ -1,45 +1,45 @@ -terms.cmi: -pp.cmi: terms.cmi -foSubst.cmi: terms.cmi -orderings.cmi: terms.cmi -foUtils.cmi: terms.cmi orderings.cmi -foUnif.cmi: terms.cmi orderings.cmi -index.cmi: terms.cmi orderings.cmi -superposition.cmi: terms.cmi orderings.cmi index.cmi -stats.cmi: terms.cmi orderings.cmi -paramod.cmi: terms.cmi orderings.cmi -nCicBlob.cmi: terms.cmi -nCicProof.cmi: terms.cmi -nCicParamod.cmi: -terms.cmo: terms.cmi -terms.cmx: terms.cmi -pp.cmo: terms.cmi pp.cmi -pp.cmx: terms.cmx pp.cmi -foSubst.cmo: terms.cmi foSubst.cmi -foSubst.cmx: terms.cmx foSubst.cmi -orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi -orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi -foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi -foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi -index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi -index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi +terms.cmi: +pp.cmi: terms.cmi +foSubst.cmi: terms.cmi +orderings.cmi: terms.cmi +foUtils.cmi: terms.cmi orderings.cmi +foUnif.cmi: terms.cmi orderings.cmi +index.cmi: terms.cmi orderings.cmi +superposition.cmi: terms.cmi orderings.cmi index.cmi +stats.cmi: terms.cmi orderings.cmi +paramod.cmi: terms.cmi orderings.cmi +nCicBlob.cmi: terms.cmi +nCicProof.cmi: terms.cmi +nCicParamod.cmi: +terms.cmo: terms.cmi +terms.cmx: terms.cmi +pp.cmo: terms.cmi pp.cmi +pp.cmx: terms.cmx pp.cmi +foSubst.cmo: terms.cmi foSubst.cmi +foSubst.cmx: terms.cmx foSubst.cmi +orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi +orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi +foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi +foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi +foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi +index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi +index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi + foUnif.cmi foSubst.cmi superposition.cmi superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ - foUnif.cmx foSubst.cmx superposition.cmi -stats.cmo: terms.cmi stats.cmi -stats.cmx: terms.cmx stats.cmi + foUnif.cmx foSubst.cmx superposition.cmi +stats.cmo: terms.cmi stats.cmi +stats.cmx: terms.cmx stats.cmi paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi + foUtils.cmi foUnif.cmi paramod.cmi paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi -nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi -nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi -nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi -nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi + foUtils.cmx foUnif.cmx paramod.cmi +nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi +nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi +nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi +nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ - nCicBlob.cmi nCicParamod.cmi + nCicBlob.cmi nCicParamod.cmi nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi + nCicBlob.cmx nCicParamod.cmi diff --git a/matita/components/ng_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt index 2633e1aba..5e055ecdc 100644 --- a/matita/components/ng_refiner/.depend.opt +++ b/matita/components/ng_refiner/.depend.opt @@ -1,25 +1,25 @@ -nDiscriminationTree.cmi: -nCicMetaSubst.cmi: -nCicUnifHint.cmi: -nCicCoercion.cmi: nCicUnifHint.cmi -nCicRefineUtil.cmi: -nCicUnification.cmi: nCicCoercion.cmi -nCicRefiner.cmi: nCicCoercion.cmi -nDiscriminationTree.cmo: nDiscriminationTree.cmi -nDiscriminationTree.cmx: nDiscriminationTree.cmi -nCicMetaSubst.cmo: nCicMetaSubst.cmi -nCicMetaSubst.cmx: nCicMetaSubst.cmi -nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi -nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicUnifHint.cmi: +nCicCoercion.cmi: nCicUnifHint.cmi +nCicRefineUtil.cmi: +nCicUnification.cmi: nCicCoercion.cmi +nCicRefiner.cmi: nCicCoercion.cmi +nDiscriminationTree.cmo: nDiscriminationTree.cmi +nDiscriminationTree.cmx: nDiscriminationTree.cmi +nCicMetaSubst.cmo: nCicMetaSubst.cmi +nCicMetaSubst.cmx: nCicMetaSubst.cmi +nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi +nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \ - nCicCoercion.cmi + nCicCoercion.cmi nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmi -nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi -nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi -nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi -nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi + nCicCoercion.cmi +nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi +nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi +nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi +nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \ - nCicCoercion.cmi nCicRefiner.cmi + nCicCoercion.cmi nCicRefiner.cmi nCicRefiner.cmx: nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi + nCicCoercion.cmx nCicRefiner.cmi diff --git a/matita/components/ng_tactics/.depend.opt b/matita/components/ng_tactics/.depend.opt index 47f203f0a..3e01ca0fb 100644 --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@ -1,28 +1,30 @@ -continuationals.cmi: -nCicTacReduction.cmi: -nTacStatus.cmi: continuationals.cmi -nCicElim.cmi: -nTactics.cmi: nTacStatus.cmi -nnAuto.cmi: nTacStatus.cmi -nDestructTac.cmi: nTacStatus.cmi -nInversion.cmi: nTacStatus.cmi -continuationals.cmo: continuationals.cmi -continuationals.cmx: continuationals.cmi -nCicTacReduction.cmo: nCicTacReduction.cmi -nCicTacReduction.cmx: nCicTacReduction.cmi -nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi -nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi -nCicElim.cmo: nCicElim.cmi -nCicElim.cmx: nCicElim.cmi -nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi -nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi +continuationals.cmi: +nCicTacReduction.cmi: +nTacStatus.cmi: continuationals.cmi +nCicElim.cmi: +nTactics.cmi: nTacStatus.cmi +nnAuto.cmi: nTacStatus.cmi +nDestructTac.cmi: nTacStatus.cmi +nInversion.cmi: nTacStatus.cmi +continuationals.cmo: continuationals.cmi +continuationals.cmx: continuationals.cmi +nCicTacReduction.cmo: nCicTacReduction.cmi +nCicTacReduction.cmx: nCicTacReduction.cmi +nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi +nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi +nCicElim.cmo: nCicElim.cmi +nCicElim.cmx: nCicElim.cmi +nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi +nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi nnAuto.cmo: nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \ - continuationals.cmi nnAuto.cmi + continuationals.cmi nnAuto.cmi nnAuto.cmx: nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ - continuationals.cmx nnAuto.cmi + continuationals.cmx nnAuto.cmi nDestructTac.cmo: nTactics.cmi nTacStatus.cmi continuationals.cmi \ - nDestructTac.cmi + nDestructTac.cmi nDestructTac.cmx: nTactics.cmx nTacStatus.cmx continuationals.cmx \ - nDestructTac.cmi -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 diff --git a/matita/components/registry/.depend.opt b/matita/components/registry/.depend.opt index 40c03891a..19a1fd325 100644 --- a/matita/components/registry/.depend.opt +++ b/matita/components/registry/.depend.opt @@ -1,3 +1,3 @@ -helm_registry.cmi: -helm_registry.cmo: helm_registry.cmi -helm_registry.cmx: helm_registry.cmi +helm_registry.cmi: +helm_registry.cmo: helm_registry.cmi +helm_registry.cmx: helm_registry.cmi diff --git a/matita/components/syntax_extensions/.depend b/matita/components/syntax_extensions/.depend index 25e67131f..119f13093 100644 --- a/matita/components/syntax_extensions/.depend +++ b/matita/components/syntax_extensions/.depend @@ -1,5 +1,5 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: -utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi -utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: +utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi +utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/matita/components/syntax_extensions/.depend.opt b/matita/components/syntax_extensions/.depend.opt index 3d7dfc21f..8f195d05a 100644 --- a/matita/components/syntax_extensions/.depend.opt +++ b/matita/components/syntax_extensions/.depend.opt @@ -1,5 +1,5 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: -utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi -utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: +utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/matita/components/thread/.depend.opt b/matita/components/thread/.depend.opt index 6616a03d0..e25145b8b 100644 --- a/matita/components/thread/.depend.opt +++ b/matita/components/thread/.depend.opt @@ -1,6 +1,6 @@ -threadSafe.cmi: -extThread.cmi: -threadSafe.cmo: threadSafe.cmi -threadSafe.cmx: threadSafe.cmi -extThread.cmo: extThread.cmi -extThread.cmx: extThread.cmi +threadSafe.cmi: +extThread.cmi: +threadSafe.cmo: threadSafe.cmi +threadSafe.cmx: threadSafe.cmi +extThread.cmo: extThread.cmi +extThread.cmx: extThread.cmi diff --git a/matita/components/xml/.depend.opt b/matita/components/xml/.depend.opt index e7e7ffbd7..eda62779f 100644 --- a/matita/components/xml/.depend.opt +++ b/matita/components/xml/.depend.opt @@ -1,6 +1,6 @@ -xml.cmi: -xmlPushParser.cmi: -xml.cmo: xml.cmi -xml.cmx: xml.cmi -xmlPushParser.cmo: xmlPushParser.cmi -xmlPushParser.cmx: xmlPushParser.cmi +xml.cmi: +xmlPushParser.cmi: +xml.cmo: xml.cmi +xml.cmx: xml.cmi +xmlPushParser.cmo: xmlPushParser.cmi +xmlPushParser.cmx: xmlPushParser.cmi diff --git a/matita/configure.ac b/matita/configure.ac index 1c7f064b9..ddd0a2b6e 100644 --- a/matita/configure.ac +++ b/matita/configure.ac @@ -5,7 +5,7 @@ AC_INIT(matita/matitaTypes.ml) 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 diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index fb6531fb0..fb48e954c 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -1,75 +1,76 @@ -applyTransformation.cmo: applyTransformation.cmi -applyTransformation.cmx: applyTransformation.cmi -buildTimeConf.cmo: -buildTimeConf.cmx: +applyTransformation.cmo: applyTransformation.cmi +applyTransformation.cmx: applyTransformation.cmi +buildTimeConf.cmo: +buildTimeConf.cmx: cicMathView.cmo: matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \ - buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi + buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi cicMathView.cmx: matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ - buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi -lablGraphviz.cmo: lablGraphviz.cmi -lablGraphviz.cmx: lablGraphviz.cmi -matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi -matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi -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: diff --git a/matita/matita/dist/ChangeLog b/matita/matita/dist/ChangeLog index 90d654b7f..866d69fda 100644 --- a/matita/matita/dist/ChangeLog +++ b/matita/matita/dist/ChangeLog @@ -1,4 +1,4 @@ -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 diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma index d6b462b10..5e34160fe 100644 --- a/matita/matita/lib/arithmetics/bigops.ma +++ b/matita/matita/lib/arithmetics/bigops.ma @@ -141,7 +141,7 @@ a ≤ b → b ≤ c → 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) bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b)) [#i #lei >plus_minus // 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. @@ -192,7 +192,7 @@ op (\big[op,nil]_{ibigop_Strue // >bigop_Strue // >bigop_Strue // - normalize assoc >comm in ⊢ (??(????%?)?) + normalize assoc >comm {⊢ (??(????%?)?)} bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse // ] @@ -263,7 +263,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2. iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) → \big[op,nil]_{ibigop_Sfalse [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //] @@ -280,7 +280,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2. |#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) @@ -298,13 +298,13 @@ qed. 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]_{ieqSc #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)) commutative_times @Hmc ] @@ -61,18 +61,18 @@ qed. 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 ⊢ (???(?(??(??%))?)) -(div_times_times ?? (n - k)) in ⊢ (???(??%)) +>associative_times {⊢ (???(?(??%)?))} +>commutative_times {⊢ (???(?(??(??%))?))} +(div_times_times ?? (n - k)) {⊢ (???(??%))} [|>(times_n_O 0) @lt_times // |@(le_plus_to_le_r k ??) associative_times in ⊢ (???(??(??%))) +>associative_times {⊢ (???(??(??%)))} >fact_minus // commutative_plus in ⊢ (???%) commutative_plus {⊢ (???%)} associative_times >(commutative_times (S k)) eq_to_eqb_true [>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) // diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma index d1afc19ee..2a9e06b0f 100644 --- a/matita/matita/lib/arithmetics/congruence.ma +++ b/matita/matita/lib/arithmetics/congruence.ma @@ -37,7 +37,7 @@ theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m. qed. theorem mod_mod : ∀n,p:nat. O

(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. @@ -79,8 +79,8 @@ 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)) (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 → @@ -228,9 +228,9 @@ 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)))) // ] ] @@ -241,10 +241,10 @@ theorem le_plus_div: ∀m,n,q. O < 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 m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %)) ->commutative_plus in ⊢ (? ? (? % ?)) >associative_plus in ⊢ (? ? %) -commutative_times {⊢ (? ? %)} (div_mod m q) {⊢ (? ? (? % ?))} >(div_mod n q) {⊢ (? ? (? ? %))} +>commutative_plus {⊢ (? ? (? % ?))} >associative_plus {⊢ (? ? %)} +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 // | //] diff --git a/matita/matita/lib/arithmetics/gcd.ma b/matita/matita/lib/arithmetics/gcd.ma index 1490a626e..8b496e9c5 100644 --- a/matita/matita/lib/arithmetics/gcd.ma +++ b/matita/matita/lib/arithmetics/gcd.ma @@ -54,7 +54,7 @@ qed. 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. @@ -69,7 +69,7 @@ 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 → @@ -182,13 +182,13 @@ theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m → n ≤ p → [(* first case *) distributive_times_plus_r - >(div_mod m n) in ⊢(? ? (? % ?) ?) + >(div_mod m n) {⊢(? ? (? % ?) ?)} >associative_times distributive_times_plus distributive_times_plus_r - >(div_mod m n) in ⊢ (? ? (? ? %) ?) + >(div_mod m n) {⊢ (? ? (? ? %) ?)} >distributive_times_plus >associative_times gcd1 in H #H +cases(eq_minus_gcd m p) #a * #b * #H >gcd1 {H} #H [@(quotient ?? (a*n-c*b)) >distributive_times_minus (commutative_times m) >commutative_times >associative_times 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 ext normalize in Hind >Hind // +#m #Hind #ext normalize >ext normalize {Hind} >Hind // #i #ltim @ext /2/ qed. diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma index c44caa7fe..7c5df29f3 100644 --- a/matita/matita/lib/arithmetics/primes.ma +++ b/matita/matita/lib/arithmetics/primes.ma @@ -480,7 +480,7 @@ change with (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. diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma index 05c13498e..274ce3d5b 100644 --- a/matita/matita/lib/basics/jmeq.ma +++ b/matita/matita/lib/basics/jmeq.ma @@ -57,14 +57,14 @@ qed. 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: @@ -77,7 +77,7 @@ qed. 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 @@ -94,7 +94,7 @@ lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0]. #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]. diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index d1dbfad77..1fdd851e0 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -30,22 +30,22 @@ lemma eq_ind_r : 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. diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index cb7c63bac..d009a63f6 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -128,15 +128,19 @@ class console ~(buffer: GText.buffer) () = 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 = @@ -415,6 +419,7 @@ class gui () = 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 @@ -867,6 +872,9 @@ class gui () = 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)) -- 2.39.2