Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

1 files changed, 24 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index e80035ad..e0d08774 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,27 @@
+Changes from V8.1gamma to V8.1
+==============================
+
+Bug fixes
+
+- Many bugs have been fixed (cf coq-bugs web page)
+
+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).
+
+Libraries
+
+- New file ConstructiveEpsilon.v defining an epsilon operator and
+  proving the axiom of choice constructively for a countable domain
+  and a decidable predicate.
+
 Changes from V8.1beta to V8.1gamma
 ==================================