diff options
Diffstat (limited to 'theories/Compat/Coq84.v')
| -rw-r--r-- | theories/Compat/Coq84.v | 3 |
1 files changed, 3 insertions, 0 deletions
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). |