From 2d5ca51f2171bc874ba0eedd32e10b55b01aa601 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 19 Oct 2000 16:06:22 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@731 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 11 ++++++++++-
 TODO    |  5 +++++
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 2dbb9f13a7..136a87d591 100644
--- a/CHANGES
+++ b/CHANGES
@@ -44,7 +44,6 @@ AstList), ou, si c'est dans une r
 
 - 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)
diff --git a/TODO b/TODO
index ab4ab0415c..5e2e6f4815 100644
--- a/TODO
+++ b/TODO
@@ -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
-- 
cgit v1.2.3