diff options
| -rw-r--r-- | CHANGES | 11 | ||||
| -rw-r--r-- | TODO | 5 |
2 files changed, 15 insertions, 1 deletions
@@ -44,7 +44,6 @@ AstList), ou, si c'est dans une règle Syntax, utiliser la quotation - Bug affichage Infix corrigé - Tactiques - Langage de tactique @@ -61,4 +60,14 @@ Tactiques en général plus son nom (sauf dans les cas "simples"). Rem : c'est une source d'incompatibilité. +Utilisation générale + +- La plupart des erreurs de typage sont maintenant localisée dans le + source (à l'exception des erreurs d'univers et de garde). + +- Rapidité accrue + +Développeurs +- Beaucoup de modification dans le sens de la simplification et de la + documentation (mais cela reste une version de transition) @@ -10,6 +10,7 @@ Environnement: - Que les Infix soit chargés lors d'un Require - Problème de compatibilité du mode implicite au discharge (avant, dépendait de l'état du mode à la création, maintenant, à la fermeture de la section) +- ajouter "parsing" aux chemins par défaut (pour g_{nat,z}syntax.cmo) Tactiques @@ -19,3 +20,7 @@ Tactiques Noyau: - Intégrer Let dans whd_* et les fonctions de tacred + +Theories: + +- remplacer Realizer par Refine ou autre chose dans TheoryList.v |