Skip to content
Snippets Groups Projects
Commit 2aa79871 authored by Ralf Jung's avatar Ralf Jung
Browse files

drop support for Coq 8.8 and 8.9

parent 7ae77142
No related branches found
No related tags found
1 merge request!190Drop support for Coq 8.8 and 8.9
......@@ -53,13 +53,3 @@ build-coq.8.10.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.10.2"
build-coq.8.9.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.1"
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
......@@ -3,6 +3,8 @@ API-breaking change is listed.
## std++ master
Coq 8.8 and 8.9 are no longer supported.
- Rename `dom_map filter``dom_filter`, `dom_map_filter_L``dom_filter_L`,
and `dom_map_filter_subseteq``dom_filter_subseteq` for consistency's sake.
- Add `max` and `min` operations for `Qp`.
......
......@@ -45,7 +45,7 @@ Notably:
This version is known to compile with:
- Coq version 8.8.2 / 8.9.1 / 8.10.2 / 8.11.2 / 8.12.0
- Coq version 8.10.2 / 8.11.2 / 8.12.0
## Installing via opam
......
......@@ -30,7 +30,7 @@ The key features of this library are as follows:
"""
depends: [
"coq" { (= "8.8.2") | (>= "8.9.1" & < "8.13~") | (= "dev") }
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -6,8 +6,7 @@ but not transitively. *)
Export Set Default Proof Using "Type".
(* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
Export Set Suggest Proof Using. *)
(* FIXME: cannot enable this on Coq 8.8.
Export Set Default Goal Selector "!". *)
Export Set Default Goal Selector "!".
(* "Fake" import to whitelist this file for the check that ensures we import
this file everywhere.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment