From 59cb5ca9b6c0e29fe65e9ae99dfd6cabafc52be6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 28 Oct 2015 15:17:30 -0400 Subject: Add compatibility Nonrecursive Elimination Schemes --- 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 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. -- cgit v1.2.3