diff options
| -rw-r--r-- | CHANGES | 9 |
1 files changed, 7 insertions, 2 deletions
@@ -1,13 +1,18 @@ Différences V7.0beta / V7.0 - Ajout de déclarations locales aux Record (record à la Randy). -- Correction de bugs (Identity Coercion; Rel not in scope of ?; - implicits in inductive defs). +- Correction de bugs + - Identity Coercion + - Rel not in scope of ? + - implicits in inductive defs + - localisation des erreurs avec Syntactif Definition - Prise en compte noms longs dans Hints, Coercions et Unfold - Rétablissement des @Definition and co - Rétablissement des token extensibles et mélangeant symboles et lettres +- Ajout d'une option Set/Unset/Test Printing Coercions - Possibilité de déplier des définitions locales à un but + Différences oubliées dans la V7.0beta : - Du fait des noms qualifiés, les variables de buts n'évitent plus les |