diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 | ||||
| -rw-r--r-- | theories/Compat/Coq84.v | 3 |
3 files changed, 19 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 diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b668239a6..8172b5771 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3293,6 +3293,16 @@ reduced to \texttt{S t}. \end{Variants} +\begin{quote} +\optindex{Refolding Reduction} +{\tt Refolding Reduction} +\end{quote} + +This option (off by default) controls the use of the refolding strategy +of {\tt cbn} while doing reductions in unification, type inference and +tactic applications. It can result in expensive unifications, as +refolding currently uses a potentially exponential heuristic. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 8ae1a9195..341be92d1 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -25,6 +25,9 @@ Global Set Nonrecursive Elimination Schemes. (** See bug 3545 *) Global Set Universal Lemma Under Conjunction. +(** Feature introduced in 8.5, disabled by default and configurable since 8.6. *) +Global Unset Refolding Reduction. + (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *) Ltac constructor_84_n n := constructor n. Ltac constructor_84_tac tac := once (constructor; tac). |