diff options
| author | Pierre-Marie Pédrot | 2016-09-14 11:40:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-14 11:40:15 +0200 |
| commit | 5e4dc9a1896a1dff832089be20cd43f4f4776869 (patch) | |
| tree | f8661480501f26b7d3dd46e064c1a6084991a280 /theories | |
| parent | 93a03345830047310d975d5de3742fa58a0a224b (diff) | |
| parent | 3e794be5f02ed438cdc5a351d09bdfb54c0be01a (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Compat/Coq84.v | 3 | ||||
| -rw-r--r-- | theories/Compat/Coq85.v | 3 |
2 files changed, 5 insertions, 1 deletions
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 8ae1a91958..341be92d1d 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). diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 54621cc1cd..0ddf1acdea 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -20,4 +20,5 @@ Global Unset Bracketing Last Introduction Pattern. Global Unset Regular Subst Tactic. Global Unset Structural Injection. Global Unset Shrink Abstract. -Global Unset Shrink Obligations.
\ No newline at end of file +Global Unset Shrink Obligations. +Global Set Refolding Reduction.
\ No newline at end of file |