diff options
author | 2016-09-12 15:14:23 +0200 | |
---|---|---|
committer | 2016-09-12 15:16:36 +0200 | |
commit | 6234ecf5f5752768175d510749cc48a97c2c0dbe (patch) | |
tree | 5af084fac65ed3ea1f2a13572b58feee0b896db3 /CHANGES | |
parent | 7a3ef81f20e159bcf4d40227d36c54abbe69c3e9 (diff) |
Refolding: disable in 8.4 compat file, document
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -28,6 +28,12 @@ Tactics - Flag "Bracketing Last Introduction Pattern" is now on by default. - Flag "Regular Subst Tactic" is now on by default. +- New flag "Refolding Reduction", now disabled by default, which turns + on refolding of constants/fixpoints (as in cbn) during the reductions + done during type inference and tactic retyping. Can be extremely + expensive. When set off, this recovers the 8.4 behaviour of unification + and type inference. Potential source of incompatibility with 8.5 developments + (the option is set on in Compat/Coq85.v). - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract tactical w.r.t. variables appearing in the body of the proof. On by default and deprecated. Minor source of incompatibility |