diff options
author | 2000-10-18 11:13:23 +0000 | |
---|---|---|
committer | 2000-10-18 11:13:23 +0000 | |
commit | e11a25974cf69d7c42bccc5e1bedc36a68b54221 (patch) | |
tree | 7e84af229ebd7b5c2e50705950990698620a30f5 /CHANGES | |
parent | c83d2687d812b8cb7202ec3555e1588f2dfdc5ff (diff) |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@719 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 12 |
1 files changed, 9 insertions, 3 deletions
@@ -2,11 +2,20 @@ Métathéorie - Ajout de définitions locales (Let-In) +Parsing + +- Le Lexeur considère maintenant comme token toute suite de symboles. + +- "command" in grammars and quotations is now "constr" as in + pretty-printing rules + + Syntaxe des constructions - Consecutive as in patterns are forbidden - Names generated in Cases are different (source d'incompatibilité) + Consecutive 'as' in patterns are forbidden - Davantage d'inférence automatique de "?". @@ -16,9 +25,6 @@ Syntaxe des constructions Vernac -- "command" in grammars and quotations is now "constr" as in - pretty-printing rules - - Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des phrases (utile pour Time et pour des grammaires abrégeant plusieurs commandes) |