From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 25 Dec 2011 13:19:42 +0100 Subject: Imported Upstream version 8.3.pl3 --- CHANGES | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index ce0763af..b8a5f9ea 100644 --- a/CHANGES +++ b/CHANGES @@ -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. -- cgit v1.2.3