mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

1 files changed, 5 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 7d34be2f83..880fa808b7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,11 @@ Tactics
   setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite).
   New syntax for declaring relations and morphisms (old syntax still working
   with minor modifications, but deprecated).
+- New implementation of the ring tactic with a built-in notion of coefficients
+  and a better usage of setoids. Previous implementation kept for compatibility
+  but is deprecated.
+- New conversion tactic "vm_compute": evaluates the goal (or an hypothesis)
+  with a call-by-value strategy, using the compiled version of terms. 
 - When rewriting H where H is not directly a Coq equality, search first H for 
   a registered setoid equality before starting to reduce in H. This is unlikely
   to break any script. Should this happen nonetheless, one can insert manually