Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for

preserving compatibility of subst after #4214 being solved.

1 files changed, 5 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 87506dadc..85a207c29 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,11 @@ Vernacular commands
 
 - New command "Redirect" to redirect the output of a command to a file.
 
+Tactics
+
+- New flag "Set Regular Subst Tactic" which fixes "subst" in situations where
+  it failed to substitute all substitutable equations or failed to simplify
+  cycles, or accidentally unfolded local definitions (flag is off by default).
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
@@ -19,7 +24,6 @@ Tactics
 - A script using the admit tactic can no longer be concluded by either
   Qed or Defined. In the first case, Admitted can be used instead. In
   the second case, a subproof should be used.
-
 - The easy tactic and the now tactical now have a more predictable
   behavior, but they might now discharge some previously unsolved goals.
 
@@ -27,25 +31,21 @@ Extraction
 
 - Definitions extracted to Haskell GHC should no longer randomly
   segfault when some Coq types cannot be represented by Haskell types.
-
 - Definitions can now be extracted to Json for post-processing.
 
 Tools
 
 - Option -I -as has been removed, and option -R -as has been
   deprecated. In both cases, option -R can be used instead.
-
 - coq_makefile now generates double-colon rules for rules such as clean.
 
 API
 
 - The interface of [change] has changed to take a [change_arg], which
   can be built from a [constr] using [make_change_arg].
-
 - [pattern_of_constr] now returns a triplet including the cleaned-up
   [evar_map], removing the evars that were turned into metas.
 
-
 Changes from V8.4 to V8.5beta1
 ==============================