summaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
commit300293c119981054c95182a90c829058530a6b6f (patch)
treed7303613741c5796b58ced7db24ec7203327dbb2 /CHANGES
parent9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff)
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES39
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.