diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-26 11:09:50 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-26 11:09:50 +0000 |
| commit | 6aaf0c643b585b173f6de4d9eb01bcf08b9aaeb1 (patch) | |
| tree | 6a26b3da928b569a953b598e10bea48f3c4f7dc5 /CHANGEMENTS | |
| parent | 3fe7c7879fb36cdcad5632fb20f893670db7c88c (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1223 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGEMENTS')
| -rw-r--r-- | CHANGEMENTS | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/CHANGEMENTS b/CHANGEMENTS index e3f6b85eb..74bf08679 100644 --- a/CHANGEMENTS +++ b/CHANGEMENTS @@ -23,6 +23,10 @@ Langage La syntaxe du "." final change (cf Vernac). Le nommage des définitions globales change (cf Métathéorie). +- Le problème avec les identificateurs se terminant par un nombre + supérieur à 2^30 est résolu. + +- Le caractère "$" n'est plus autorisé dans les identificateurs. Extensions de syntaxe avec Grammar et Syntax @@ -79,7 +83,7 @@ Syntaxe des constructions Commandes -- Changement de noms de certaines commandes +- Changement de nom de certaines commandes AddPath -> Add LoadPath; Print LoadPath -> Print LoadPath; @@ -135,7 +139,7 @@ Tactiques d'un tel language et se procurer une documentation provisoire de Ltac, se référer à l'URL suivante: - http://pauillac.inria.fr/~delahaye/ + http://logical.inria.fr/~delahaye/ - Tactique Let renommé en LetTac et utilise le let-in primitif; Induction renommé en OldInduction et nouveau Induction plus |