diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2015-10-28 15:17:30 -0400 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-04-04 17:06:20 +0200 |
| commit | 59cb5ca9b6c0e29fe65e9ae99dfd6cabafc52be6 (patch) | |
| tree | da787a260b837ddc40977982bb29eeca3c40865c /theories/Compat | |
| parent | 856780b163fdcd5e36a1d4af99034e3af6fde1d7 (diff) | |
Add compatibility Nonrecursive Elimination Schemes
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. |