From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 19 Jan 2006 22:34:29 +0000 Subject: Imported Upstream version 8.0pl3 --- CHANGES | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) (limited to 'CHANGES') 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 =============================== -- cgit v1.2.3