1 files changed, 17 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 2daeded1..7b0a41d0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,20 @@
+Changes from V8.0pl1 to V8.0pl2
+===============================
+
+Notations
+
+- Option "format" now aware of recursive notations
+
+Bug fixes
+
+- Tactic "fail n" for n<>0 now works (notice that each "match term with"
+  block decreases the failure level, in accordance with the intuition but
+  not in conformity with the reference manual)
+- Option -dump-glob now strips module segment as expected by coqdoc (which
+  is still not aware of modules)
+- See coq-bugs web page for a full list of fixed bugs (look for
+  fixes committed before Jan 2005 to cvs version V8-0-bugfix)
+
 Changes from V8.0 to V8.0pl1
 ============================