From cbe9f6c3d08bd854a0908448e6085505b67851c8 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 21 May 2002 20:09:11 +0000
Subject: Field + MapleMode

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

diff --git a/CHANGES b/CHANGES
index a44de5eb09..ef2ae861ea 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,6 +20,8 @@ Tactics
 - Pattern now working on partially applied subterms
 - Ring no longer applies irreversible congruence laws of mult but
   better applies congruence laws of plus (slight source of incompatibilities).
+- Field now accepts terms to be simplified as arguments (as for Ring). This
+  extension has been also implemented using the toplevel tactic language.
 - Intuition does no longer unfold constants except "<->" and "~". It
   can be parameterized by a tactic. It also can introduce dependent
   product if needed (source of incompatibilities)
@@ -57,7 +59,8 @@ Tools
 User Contributions
 
 - CongruenceClosure (congruence closure decision procedure)
-- MapleMode (an interface to embed Maple simplification procedures in Coq)
+- MapleMode (an interface to embed Maple simplification procedures over
+  rational fractions in Coq)
 - Chinese has been rewritten using Z from ZArith as datatype
   ZChinese is the new version, Chinese the obsolete one
 
-- 
cgit v1.2.3