diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 33 |
1 files changed, 33 insertions, 0 deletions
@@ -1,10 +1,36 @@ +Changes from V8.3pl3 to V8.3pl4 +=============================== + +Bug fixes: + +- #2724 (using notations with binders in cases patterns was provoking an anomaly) +- #2723 (alpha-conversion bug #2723 introduced in r12485-12486) +- #2732 (anomaly when using the tolerance for writing "f atomic_tac" + as a short-hand for "f ltac:(atomic_tac)") +- #2729 (vm_compute: function used to decompose constructors did not handle let-ins) +- #2728 (compatibility with camlp5 6.05) +- #2682 (Fail discard the effects of a successful command) +- #2703 (Undetected universe inconsistency) +- #2667 (Coq crashes when "Arguments Scope" has too many parameters) +- Compilation of coqide under MacOS with gtk >= 2.24.11 +- Coqdoc: Fixing missing newline when using "Proof term." + + Changes from V8.3pl2 to V8.3pl3 =============================== +The following (non exhaustive) list of bugs have been fixed: + General - #2411 (Axiom / Hypothesis / Variable allowed again during proofs) - #2603 (verify that all names of an inductive block aren't already used) +- #1804 (pattern-matching compilation bug with highly nested sigma-types) +- #2615 (anomaly in inferring pattern-matching return type) +- #2504 (bug in computing universe of polymorphic inductive types) +- #2407 (stack overflow in Function) +- #2181 (unnamed but dependent fields in Classes) +- bug with modules in virtual machine Modules @@ -17,6 +43,7 @@ Tactics - #2467, #2464 (fixes for fsetdec) - Document the "appcontext" variant of "context" that better handles partial applications. +- #2640 (ltac anomaly in expecting a tactic and finding a definition) Coqide @@ -35,6 +62,12 @@ Extraction - Forbid Prop-universe-polymorphism of inductive when extracting to ocaml, otherwise things may fail badly (report by S. Glondu). +Coqdoc + +- #2606 (bad processing of coq escaped in comments) +- #2423 (handling of -R in coqdoc) +- fixing garbage when using some greek letters as identifier names + Changes from V8.3pl1 to V8.3pl2 =============================== |