MAJ ring

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9569 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 1 deletions

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
 ==================================