diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 39 |
1 files changed, 38 insertions, 1 deletions
@@ -1,3 +1,40 @@ +Changes from V8.3pl2 to V8.3pl3 +=============================== + +General + +- #2411 (Axiom / Hypothesis / Variable allowed again during proofs) +- #2603 (verify that all names of an inductive block aren't already used) + +Modules + +- #2608 (better handling of inlining and aliases, avoiding a Not_found) +- #2168 (Print Assumption now support opaque modules) +- #2609 (avoid adding twice a module in the environment in coqchk) + +Tactics + +- #2467, #2464 (fixes for fsetdec) +- Document the "appcontext" variant of "context" that better handles + partial applications. + +Coqide + +- #2363 (fix the command separator for external commands) +- #2499 (fix remove_current_view_page) +- #2357 (allow the use of Abort) + +Extraction + +- #2540 (global references should be indexed on their user parts) +- #2556 (support of records with anonymous fields) +- #2565 (typo in the documentation) +- #2570 (avoid internal eta-reduction) +- #2552 (For Haskell, type signature for __ and unsafeCoerce) +- For Haskell, avoid some sources of useless unsafeCoerce +- Forbid Prop-universe-polymorphism of inductive when extracting + to ocaml, otherwise things may fail badly (report by S. Glondu). + Changes from V8.3pl1 to V8.3pl2 =============================== @@ -122,7 +159,7 @@ Automation tactics - Tactic "intuition" now preserves inner "iff" and "not" (exceptional source of incompatibilities solvable by redefining "intuition" as - "unfold iff, not in *; intuition", or by using "Set Intuition Unfolding".) + "unfold iff, not in *; intuition", or by using "Set Intuition Iff Unfolding".) - Tactic "tauto" now proves classical tautologies as soon as classical logic (i.e. library Classical_Prop or Classical) is loaded. - Tactic "gappa" has been removed from the Dp plugin. |