diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-04 20:11:03 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-09 23:48:15 +0100 |
commit | c803bb6cc31134f0759ecf06d5411ce812e05e54 (patch) | |
tree | dc70ab174df5dd753b68fc51f2e4afd7e54d85c5 /CHANGES | |
parent | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (diff) |
[doc] Document removal of deprecated options.
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 17 |
1 files changed, 17 insertions, 0 deletions
@@ -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 =========================== |