diff options
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 90083b00d..d695ef1d8 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -15,6 +15,9 @@ Ltac omega := Coq.omega.Omega.omega. (** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *) Global Set Asymmetric Patterns. +(** The automatic elimination schemes for records were dropped by default in 8.5. This restores the default behavior of Coq 8.4. *) +Global Set Nonrecursive Elimination Schemes. + (** See bug 3545 *) Global Set Universal Lemma Under Conjunction. |