From 9fa62e2a3230aef081c2b0f6b382ac3fcd29b6e0 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 18 Sep 2001 12:05:46 +0000
Subject: Modif pour Ltac et ajout de Field

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1978 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/CHANGES b/CHANGES
index 6c6962ebc5..60643cd086 100644
--- a/CHANGES
+++ b/CHANGES
@@ -275,11 +275,8 @@ Tactiques
 - Langage de tactiques Ltac: nouvelle couche de métalangage pour traiter de
   petites automatisations. C'est essentiellement un petit noyau fonctionnel
   muni d'opérateurs de filtrage élaborés (sur les termes, les contextes de
-  preuves et réalisant du backtracking). Pour connaître les justifications
-  d'un tel language et se procurer une documentation provisoire de Ltac, se
-  référer à l'URL suivante:
-
-      http://logical.inria.fr/~delahaye/
+  preuves et réalisant du backtracking). Pour plus détails, consulter le
+  manuel de référence (chapitre 10).
 
 - Tactique Let renommé en LetTac et utilise le let-in primitif;
   Induction renommé en OldInduction et nouveau Induction plus
@@ -314,6 +311,9 @@ Tactiques
 - Les instantiations redondantes ou incompatibles de Apply ... with ...
   sont maintenant correctement traitées.
 
+- Nouveau: tactique Field pour décider des égalités sur les corps commutatifs.
+  La tactique a été instantiée pour les nombres réels et peut donc être
+  utilisée pour résoudre des égalités sur les réels.
 
 Outils
 
-- 
cgit v1.2.3