From 13e17eac2e476114305472e581a433d8c08d48d6 Mon Sep 17 00:00:00 2001
From: courant
Date: Thu, 13 Sep 2001 07:36:23 +0000
Subject: explications modifications Tauto

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

diff --git a/CHANGES b/CHANGES
index 2621b025be..e5cbd286f9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,9 @@
 Modifications depuis la V7.0
 
+- Tauto considère de façon uniforme les égalités : un but contenant des
+  égalités de la forme "t=t" sera résolu de la même façon que si toutes
+  ces égalités étaient remplacées par "True". En particulier, Tauto résout
+  tous les buts de la forme "H : ~ t = t |- A".
 - Fonctions de réduction dans les définitions locales s'appliquent par
   défaut au corps de la définition. Extension de la notion de Clause
   pour forcer l'action sur le type des défs seulement sous la forme
-- 
cgit v1.2.3