diff options
author | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
commit | 0c0eeea26aafd36301d4b5592225e34153ff955f (patch) | |
tree | 1d839759bc9efc76ab3a0e09a5b52aa3039fffc7 /CHANGES | |
parent | 46af7a39c66bc711fb32a5ce4fed4ab4f218d6af (diff) | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Merge commit 'upstream/8.0pl3'
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 =============================== |