diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2015-11-10 13:06:31 -0500 |
|---|---|---|
| committer |  Jason Gross <jgross@mit.edu> | 2016-01-12 14:33:47 -0500 |
| commit | 8a049d8a6fa785190ac66f2840f27699f13efd89 (patch) | |
| tree | 2e64fb0675062a79770624a293b3263ac70bde4c /theories/Compat | |
| parent | 51b2581d027528c8e4a347f157baf51a71b9d613 (diff) | |
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.
Diffstat (limited to 'theories/Compat')
| -rw-r--r-- | theories/Compat/Coq84.v | 4 |
1 files changed, 4 insertions, 0 deletions
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. |