]> matita.cs.unibo.it Git - helm.git/commit
Much ado about nothing:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Apr 2007 14:46:36 +0000 (14:46 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Apr 2007 14:46:36 +0000 (14:46 +0000)
commitcd91767a396b7bbc72e6e3ee90a3b758421f935d
tree4608ce891383e8d25aa81e7320b104b8e1518553
parent324d594e5e37081d945d631986447a95a1937634
Much ado about nothing:
 1) repeat tac end ==> repeat tac
 2) do n tac end   ==> do n tac
 3) "goal n" finally dropped (deprecated, semantics no longer clear)
 4) the AST (in grafiteAst) has been changed to better reflect the
    distinction between tactics (including h.o. tactics, i.e. tacticals),
    punctuational tinycals and non punctuation tinycals (i.e. skip, focus,
    unfocus)
 5) all tacticals are now running properly in every condition;
    but tacticals argument (i.e. tactics occurring in tacticals) are
    disambiguated eagerly and not lazily (to be changed)

WARNING: the code in proceduralTypes.ml has been commented out since I am
not able to figure out how to fix it properly
24 files changed:
components/acic_procedural/proceduralTypes.ml
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite/grafiteAstPp.mli
components/grafite_engine/grafiteEngine.ml
components/grafite_parser/grafiteDisambiguate.ml
components/grafite_parser/grafiteParser.ml
components/tactics/fourierR.ml
components/tactics/proofEngineStructuralRules.ml
components/tactics/proofEngineStructuralRules.mli
components/tactics/ring.ml
components/tactics/tacticals.ml
components/tactics/tacticals.mli
components/tactics/tactics.ml
components/tactics/tactics.mli
components/tptp_grafite/tptp2grafite.ml
matita/help/C/sec_tacticals.xml
matita/library/nat/div_and_mod.ma
matita/library/nat/factorization.ma
matita/library/nat/minus.ma
matita/library/nat/orders.ma
matita/matitaGui.ml
matita/matitaMathView.ml
matita/matitaScript.ml