Commit 5f134375 authored by Robbert Krebbers's avatar Robbert Krebbers

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.
parent b34d006a
Pipeline #12726 passed with stage
in 6 minutes and 26 seconds
......@@ -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"
......@@ -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
......
......@@ -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") }
]
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment