From 9ca92150efd64e50dd5dd6eb84d820e1db669706 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 2 Feb 2024 10:24:23 +0100
Subject: [PATCH] test on Coq 8.19
---
.gitlab-ci.yml | 13 ++++++++++---
CHANGELOG.md | 2 ++
README.md | 2 +-
_CoqProject | 2 ++
4 files changed, 15 insertions(+), 4 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f4c304e7..eefc66ac 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -45,10 +45,10 @@ variables:
## Build jobs
# The newest version runs with timing.
-build-coq.8.18.0:
+build-coq.8.19.0:
<<: *template
variables:
- OPAM_PINS: "coq version 8.18.0"
+ OPAM_PINS: "coq version 8.19.0"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
CI_COQCHK: "1"
@@ -59,9 +59,16 @@ build-coq.8.18.0:
interruptible: false
# The newest version also runs in MRs, without timing.
-build-coq.8.18.0-mr:
+build-coq.8.19.0-mr:
<<: *template
<<: *only_mr
+ variables:
+ OPAM_PINS: "coq version 8.19.0"
+ DENY_WARNINGS: "1"
+ MANGLE_NAMES: "1"
+
+build-coq.8.18.0:
+ <<: *template
variables:
OPAM_PINS: "coq version 8.18.0"
DENY_WARNINGS: "1"
diff --git a/CHANGELOG.md b/CHANGELOG.md
index fd80ae59..d5e6f775 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,8 @@ API-breaking change is listed.
## 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`
before proving the goal by reflexivity.
- Add new typeclass `MThrow E M` to generally represent throwing an error of
diff --git a/README.md b/README.md
index 8885a951..4b427400 100644
--- a/README.md
+++ b/README.md
@@ -43,7 +43,7 @@ Notably:
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
older versions will be dropped when it is convenient.
diff --git a/_CoqProject b/_CoqProject
index 2b206438..5898a24d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,8 @@
-Q stdpp_unstable stdpp.unstable
# Fixing this one requires Coq 8.17
-arg -w -arg -future-coercion-class-field
+# Fixing this one requires Coq 8.19
+-arg -w -arg -argument-scope-delimiter
stdpp/options.v
stdpp/base.v
--
GitLab