Merge branch 'v8.5' into v8.6

1 files changed, 3 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 8f873bd91..17e397d6e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -626,6 +626,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").
@@ -1164,9 +1167,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