From 6234ecf5f5752768175d510749cc48a97c2c0dbe Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 12 Sep 2016 15:14:23 +0200 Subject: Refolding: disable in 8.4 compat file, document --- theories/Compat/Coq84.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'theories/Compat') 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). -- cgit v1.2.3