From 5ef642ad47de7ff465ea2d5456c387fd35409539 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 31 Jul 2016 15:49:29 +0200
Subject: Fixing CHANGES.

Option Standard Proposition Elimination Scheme from 8.5 was not
documented in the right section.
---
 CHANGES | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index c74aa7234c..de9dc649cb 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
 
-- 
cgit v1.2.3