Imported Upstream version 8.0pl3upstream/8.0pl3

1 files changed, 43 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 7b0a41d0..7c7f5dc7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,46 @@
+Changes from V8.0pl2 to V8.0pl3
+===============================
+
+Tactics
+
+- The search depth argument of auto can be parameterised in the
+  Ltac language
+- Added entry constr_may_eval for tactic extensions (new syntax)
+
+Compilation
+
+- Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0.
+
+Standard library
+
+- A couple of lemmas of ZArith were renamed. This concerns names
+  containing O (the letter), which is replaced by 0 (the number).
+
+Bug fixes
+
+- Fixes a serious bug in CoqIde. The windows port should be able
+  to load large libraries (such as Reals) without producing the
+  "bad file descriptor" error.
+- Scope of Ltac variables: global Ltac macros no longer hide goal
+  hypotheses
+- Many fixes concerning extraction: 
+  * fewer useless eta-expansions
+  * for Ocaml: extraction of records should be ok now. Problem with 
+    type t = M.t in modules fixed.
+  * in Haskell: improved use of unsafeCoerce, fixed Extract Constant, 
+    function types are now printed.
+  * important revision of the Scheme extraction: 
+    see http://www.pps.jussieu.fr/~letouzey/scheme
+- Fixes a bug in the interpretation of record projections ("bad number
+  of parameters" error)
+- Fixed a bug in the omega tactic
+- Fixed a bug in the fold tactic regarding hypotheses ordering
+- Pretty-print of universes fixed
+- Added an empty level 99 in patterns syntax entry
+- "Notation" bug fixes ("only parsing" bug, printing of numerals
+  arguments of coercions, default spacing for recursive notations
+  with no terminal separator, "Tactic Notation" printer).
+
 Changes from V8.0pl1 to V8.0pl2
 ===============================