Fixing CHANGES.

Option Standard Proposition Elimination Scheme from 8.5 was not
documented in the right section.

1 files changed, 3 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index c74aa7234..de9dc649c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -533,6 +533,9 @@ Tactics
 - Behavior of introduction patterns -> and <- made more uniform
   (hypothesis is cleared, rewrite in hypotheses and conclusion and
   erasing the variable when rewriting a variable).
+- New experimental option "Set Standard Proposition Elimination Names"
+  so that case analysis or induction on schemes in Type containing
+  propositions now produces "H"-based names.
 - Tactics from plugins are now active only when the corresponding module
   is imported (source of incompatibilities, solvable by adding an "Import";
   in the particular case of Omega, use "Require Import OmegaTactic").
@@ -1071,9 +1074,6 @@ Other tactics
   clears (resp. reverts) H and all the hypotheses that depend on H.
 - Ltac's pattern-matching now supports matching metavariables that
   depend on variables bound upwards in the pattern.
-- New experimental option "Set Standard Proposition Elimination Names"
-  so that case analysis or induction on schemes in Type containing
-  propositions now produces "H"-based names.
 
 Tactic definitions