aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-10-19 16:06:22 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-10-19 16:06:22 +0000
commit2d5ca51f2171bc874ba0eedd32e10b55b01aa601 (patch)
tree220b9feb764fb12991dab49a48718eefe51ab5dc /CHANGES
parentd3e2f28966bb6d3e5766b3da2ee333cdc3438b13 (diff)
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@731 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES11
1 files changed, 10 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 2dbb9f13a..136a87d59 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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)