aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-04 20:11:03 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-09 23:48:15 +0100
commitc803bb6cc31134f0759ecf06d5411ce812e05e54 (patch)
treedc70ab174df5dd753b68fc51f2e4afd7e54d85c5 /CHANGES
parent5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff)
[doc] Document removal of deprecated options.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES17
1 files changed, 17 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 441154b3a..399e62de5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -145,6 +145,23 @@ Compatibility support
- Support for compatibility with versions before 8.6 was dropped.
+Options
+
+- The following deprecated options have been removed:
+
+ + `Refolding Reduction`
+ + `Standard Proposition Elimination`
+ + `Discriminate Introduction`
+ + `Shrink Abstract`
+ + `Tactic Pattern Unification`
+ + `Intuition Iff Unfolding`
+ + `Injection L2R Pattern Order`
+ + `Record Elimination Schemes`
+ + `Match Strict`
+ + `Typeclasses Legacy Resolution`
+ + `Typeclasses Module Eta`
+ + `Typeclass Resolution After Apply`
+
Changes from 8.7.1 to 8.7.2
===========================