diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-09-12 15:14:23 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-09-12 15:16:36 +0200 |
| commit | 6234ecf5f5752768175d510749cc48a97c2c0dbe (patch) | |
| tree | 5af084fac65ed3ea1f2a13572b58feee0b896db3 /theories/Compat | |
| parent | 7a3ef81f20e159bcf4d40227d36c54abbe69c3e9 (diff) | |
Refolding: disable in 8.4 compat file, document
Diffstat (limited to 'theories/Compat')
| -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). |