From 8a049d8a6fa785190ac66f2840f27699f13efd89 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 10 Nov 2015 13:06:31 -0500 Subject: Update Coq84.v Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. --- theories/Compat/Coq84.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'theories/Compat') diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 1c70a894a..729687636 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -7,6 +7,10 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.4 *) + +(** Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. *) +Require Export Coq.Compat.Coq85. + (** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *) (** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available. But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *) Require Coq.omega.Omega. -- cgit v1.2.3