]> matita.cs.unibo.it Git - helm.git/commit
new, more rigid syntax, for auto_params affecting the declarative language.
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 May 2008 14:01:04 +0000 (14:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 26 May 2008 14:01:04 +0000 (14:01 +0000)
commitfd93fa0155994b70482e0f07d8e45c238cce835d
treea8d15604de899fd3f68e2786847e0ad3c34fdaf8
parentd0e058e37a75dcb0247b0b0efbe99e68ce1ceca4
new, more rigid syntax, for auto_params affecting the declarative language.

many multi-word constructs (like 'we proved') are now a single token.
all declarative tactics now use auto_params.
syntax of declarative tactics changed.
many camlp5 refactoring to avoid many rule conflics.
16 files changed:
helm/software/components/content_pres/cicNotationLexer.ml
helm/software/components/content_pres/cicNotationParser.ml
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
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/declarative.ml
helm/software/components/tactics/declarative.mli
helm/software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma
helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma
helm/software/matita/contribs/dama/dama_didactic/reals.ma
helm/software/matita/help/C/sec_terms.xml
helm/software/matita/library/demo/power_derivative.ma
helm/software/matita/matitaGui.ml
helm/software/matita/tests/decl.ma