]> 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)
commit50afaf262195266d156f594cff7e92a6e8898b3e
tree5f050bbb87d751044cd707ea827ddfcbb3ab61ce
parenta4ea24a127fa391d3b65f15e18db5af138f14ed2
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:
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite/grafiteAstPp.mli
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/fourierR.ml
helm/software/components/tactics/proofEngineStructuralRules.ml
helm/software/components/tactics/proofEngineStructuralRules.mli
helm/software/components/tactics/ring.ml
helm/software/components/tactics/tacticals.ml
helm/software/components/tactics/tacticals.mli
helm/software/components/tactics/tactics.ml
helm/software/components/tactics/tactics.mli
helm/software/components/tptp_grafite/tptp2grafite.ml
helm/software/matita/help/C/sec_tacticals.xml
helm/software/matita/library/nat/div_and_mod.ma
helm/software/matita/library/nat/factorization.ma
helm/software/matita/library/nat/minus.ma
helm/software/matita/library/nat/orders.ma
helm/software/matita/matitaGui.ml
helm/software/matita/matitaMathView.ml
helm/software/matita/matitaScript.ml