From 785d73cfdab0e3dfdc6c12098fc9e94023eae34f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 31 Jan 2007 17:01:38 +0000
Subject: MAJ ring

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

diff --git a/CHANGES b/CHANGES
index 4331f3f651..9101ace269 100644
--- a/CHANGES
+++ b/CHANGES
@@ -2,7 +2,18 @@ Changes from V8.1gamma to ...
 =============================
 
 - Added option Global to "Implicit Arguments" and "Arguments Scope" for
-  section surviving
+  section surviving.
+
+Tactics
+
+- New tactic ring, ring_simplify and new tactic field now able to manage
+  power to a positive integer constant. Tactic ring on Z and R, and
+  field on R manage power (may lead to incompatibilities with V8.1gamma).
+- Tactic field_simplify now applicable in hypotheses.
+- New field_simplify_eq for simplifying field equations into ring equations.
+- Tactics ring, ring_simplify, field, field_simplify and field_simplify_eq 
+  all able to apply user-given equations to rewrite monoms on the fly 
+  (see documentation).
 
 Changes from V8.1beta to V8.1gamma
 ==================================
-- 
cgit v1.2.3