diff options
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | TODO | 1 | ||||
| -rw-r--r-- | dev/changements.txt | 3 |
3 files changed, 9 insertions, 2 deletions
@@ -1,8 +1,11 @@ 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 ?). +- Correction de bugs (Identity Coercion; Rel not in scope of ?; + implicits in inductive defs). +- Prise en compte noms longs dans Hints et Coercions +- Rétablissement des @Definition and co +- Rétablissement des token extensibles et mélangeant symboles et lettres ---------------------------------------------------------------------- English version of changes is available on @@ -39,3 +39,4 @@ Doc: - clarifier la sémantique de Decompose (i.e. travaille pas sous les ->) - faut-il mieux spécifier la sémantique de Simpl (??) - vérifier si Print Table id est à jour +- documenter @Definition and co diff --git a/dev/changements.txt b/dev/changements.txt index 00bfa46637..cc5025c9c3 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -156,6 +156,9 @@ Changements dans les fonctions : ex-Tradevar, maintenant Evarutil mt_tycon -> empty_tycon + Recordops + struc_info -> find_structure + Changements dans les inductifs ------------------------------ Nouveaux types "constructor" et "inductive" dans Term |