diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-06 21:54:02 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-06 21:54:02 +0200 |
| commit | 56e18308ce47ee2fdf5e8d1ad87a1e8c1b67a76e (patch) | |
| tree | 7414cc3c4fa765dd410421d7df17cca1faad192a /theories/Compat | |
| parent | 47bf10e0216f7736ffe7921ce74d620594bcfcba (diff) | |
| parent | 8a049d8a6fa785190ac66f2840f27699f13efd89 (diff) | |
Merge remote-tracking branch 'github/pr/118' into trunk
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 aa4411704..39bc59a65 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. |