Imported Upstream version 8.3.pl3upstream/8.3.pl3

1 files changed, 38 insertions, 1 deletions

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.