1
Changes from V8.3pl2 to V8.3pl3
2
===============================
6
- #2411 (Axiom / Hypothesis / Variable allowed again during proofs)
7
- #2603 (verify that all names of an inductive block aren't already used)
11
- #2608 (better handling of inlining and aliases, avoiding a Not_found)
12
- #2168 (Print Assumption now support opaque modules)
13
- #2609 (avoid adding twice a module in the environment in coqchk)
17
- #2467, #2464 (fixes for fsetdec)
18
- Document the "appcontext" variant of "context" that better handles
23
- #2363 (fix the command separator for external commands)
24
- #2499 (fix remove_current_view_page)
25
- #2357 (allow the use of Abort)
29
- #2540 (global references should be indexed on their user parts)
30
- #2556 (support of records with anonymous fields)
31
- #2565 (typo in the documentation)
32
- #2570 (avoid internal eta-reduction)
33
- #2552 (For Haskell, type signature for __ and unsafeCoerce)
34
- For Haskell, avoid some sources of useless unsafeCoerce
35
- Forbid Prop-universe-polymorphism of inductive when extracting
36
to ocaml, otherwise things may fail badly (report by S. Glondu).
1
38
Changes from V8.3pl1 to V8.3pl2
2
39
===============================
123
160
- Tactic "intuition" now preserves inner "iff" and "not" (exceptional
124
161
source of incompatibilities solvable by redefining "intuition" as
125
"unfold iff, not in *; intuition", or by using "Set Intuition Unfolding".)
162
"unfold iff, not in *; intuition", or by using "Set Intuition Iff Unfolding".)
126
163
- Tactic "tauto" now proves classical tautologies as soon as classical logic
127
164
(i.e. library Classical_Prop or Classical) is loaded.
128
165
- Tactic "gappa" has been removed from the Dp plugin.
added
removed
CHANGES
