summaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES43
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
===============================