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

test on Coq 8.19

parent dd93e4c3
Branches
Tags
1 merge request!538test on Coq 8.19
Pipeline #96082 passed
...@@ -45,10 +45,10 @@ variables: ...@@ -45,10 +45,10 @@ variables:
## Build jobs ## Build jobs
# The newest version runs with timing. # The newest version runs with timing.
build-coq.8.18.0: build-coq.8.19.0:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version 8.18.0" OPAM_PINS: "coq version 8.19.0"
DENY_WARNINGS: "1" DENY_WARNINGS: "1"
MANGLE_NAMES: "1" MANGLE_NAMES: "1"
CI_COQCHK: "1" CI_COQCHK: "1"
...@@ -59,9 +59,16 @@ build-coq.8.18.0: ...@@ -59,9 +59,16 @@ build-coq.8.18.0:
interruptible: false interruptible: false
# The newest version also runs in MRs, without timing. # The newest version also runs in MRs, without timing.
build-coq.8.18.0-mr: build-coq.8.19.0-mr:
<<: *template <<: *template
<<: *only_mr <<: *only_mr
variables:
OPAM_PINS: "coq version 8.19.0"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
build-coq.8.18.0:
<<: *template
variables: variables:
OPAM_PINS: "coq version 8.18.0" OPAM_PINS: "coq version 8.18.0"
DENY_WARNINGS: "1" DENY_WARNINGS: "1"
......
...@@ -3,6 +3,8 @@ API-breaking change is listed. ...@@ -3,6 +3,8 @@ API-breaking change is listed.
## std++ master ## std++ master
Coq 8.19 is newly supported by this version of std++.
- Add `TCSimpl` type class that is similar to `TCEq` but performs `simpl` - Add `TCSimpl` type class that is similar to `TCEq` but performs `simpl`
before proving the goal by reflexivity. before proving the goal by reflexivity.
- Add new typeclass `MThrow E M` to generally represent throwing an error of - Add new typeclass `MThrow E M` to generally represent throwing an error of
......
...@@ -43,7 +43,7 @@ Notably: ...@@ -43,7 +43,7 @@ Notably:
This version is known to compile with: This version is known to compile with:
- Coq version 8.16.1 / 8.17.1 / 8.18.0 - Coq version 8.16.1 / 8.17.1 / 8.18.0 / 8.19.0
Generally we always aim to support the last two stable Coq releases. Support for Generally we always aim to support the last two stable Coq releases. Support for
older versions will be dropped when it is convenient. older versions will be dropped when it is convenient.
......
...@@ -4,6 +4,8 @@ ...@@ -4,6 +4,8 @@
-Q stdpp_unstable stdpp.unstable -Q stdpp_unstable stdpp.unstable
# Fixing this one requires Coq 8.17 # Fixing this one requires Coq 8.17
-arg -w -arg -future-coercion-class-field -arg -w -arg -future-coercion-class-field
# Fixing this one requires Coq 8.19
-arg -w -arg -argument-scope-delimiter
stdpp/options.v stdpp/options.v
stdpp/base.v stdpp/base.v
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment