diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 43 |
1 files changed, 43 insertions, 0 deletions
@@ -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 =============================== |