From 5f1343752b3bac6729cdc1491f0f21f65c9f000c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Nov 2018 11:42:10 +0100
Subject: [PATCH] Drop support for Coq 8.6.
MR #41 relies on https://github.com/coq/coq/issues/5039, which has
not been fixed in Coq 8.6.
---
.gitlab-ci.yml | 9 ---------
README.md | 10 +++++-----
opam | 2 +-
3 files changed, 6 insertions(+), 15 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e326bbff..1de5533e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -78,12 +78,3 @@ build-coq.8.7.0:
variables:
OPAM_PINS: "coq version 8.7.0"
-build-coq.8.6.1:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.6.1"
-
-build-coq.8.6.0:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.6"
diff --git a/README.md b/README.md
index 2dbdd671..54b64627 100644
--- a/README.md
+++ b/README.md
@@ -33,19 +33,19 @@ Notably:
* The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
`Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`. See
[`base.v`](theories/base.v) for further details.
-* It blocks `simpl` on all operations on integers `Z` (by setting
+* It blocks `simpl` on all operations involving integers `Z` (by setting
`Arguments op : simpl never`). We do this because `simpl` tends to expose
- their internals (e.g. try `simpl` on `Z.of_nat (S n) + y`).
+ the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
As a consequence of blocking `simpl`, due to
[Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
- sometimes fails. We do not consider this an issue since we use `lia` (for
- which the aforementioned Coq bug was fixed) instead of `omega` anywhere.
+ becomes unreliable. We do not consider this an issue since we use `lia` (for
+ which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
## Prerequisites
This version is known to compile with:
- - Coq version 8.6.0 / 8.6.1 / 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
+ - Coq version 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
## Installing via opam
diff --git a/opam b/opam
index a53b1619..a12aba63 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
depends: [
- "coq" { (>= "8.6" & < "8.10~") | (= "dev") }
+ "coq" { (>= "8.7" & < "8.10~") | (= "dev") }
]
--
GitLab