From 986df0d59cf4eea6379451c282529ce0aa2095ab Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Thu, 28 Dec 2023 17:11:17 +0100
Subject: [PATCH] compatibility for coq-community packages with 8.19

---
 .../coq-almost-full.8.18.0/opam               | 38 +++++++++++++++++++
 .../coq-high-school-geometry.8.16.0/opam      |  2 +-
 .../coq-huffman/coq-huffman.8.16.0/opam       |  2 +-
 .../coq-jmlcoq/coq-jmlcoq.8.15.0/opam         |  2 +-
 .../coq-sudoku/coq-sudoku.8.16.0/opam         |  2 +-
 5 files changed, 42 insertions(+), 4 deletions(-)
 create mode 100644 released/packages/coq-almost-full/coq-almost-full.8.18.0/opam

diff --git a/released/packages/coq-almost-full/coq-almost-full.8.18.0/opam b/released/packages/coq-almost-full/coq-almost-full.8.18.0/opam
new file mode 100644
index 0000000000..646ffbb3af
--- /dev/null
+++ b/released/packages/coq-almost-full/coq-almost-full.8.18.0/opam
@@ -0,0 +1,38 @@
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/almost-full"
+dev-repo: "git+https://github.com/coq-community/almost-full.git"
+bug-reports: "https://github.com/coq-community/almost-full/issues"
+license: "MIT"
+
+synopsis: "Almost-full relations in Coq for proving termination"
+description: """
+Coq development of almost-full relations, including the Ramsey
+Theorem, useful for proving termination."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.11" & < "8.20"}
+]
+
+tags: [
+  "category:Computer Science/Data Types and Data Structures"
+  "keyword:Ramsey theorem"
+  "keyword:termination"
+  "keyword:almost-full relations"
+  "keyword:well-founded relations"
+  "logpath:AlmostFull"
+  "date:2023-12-28"
+]
+authors: [
+  "Dimitrios Vytiniotis"
+  "Thierry Coquand"
+  "David Wahlstedt"
+]
+
+url {
+  src: "https://github.com/coq-community/almost-full/releases/download/v8.18.0/almost-full-8.18.0.tar.gz"
+  checksum: "sha512=c6871611ae19c34dfd6c27f86c29c9b38cff126cc2631684357a3cf04bb5d38e8aed0d4178f26f9c584e16cda7c6c6d1422996c0b057fe7fd8f5470662d284b3"
+}
diff --git a/released/packages/coq-high-school-geometry/coq-high-school-geometry.8.16.0/opam b/released/packages/coq-high-school-geometry/coq-high-school-geometry.8.16.0/opam
index a27b7e91bd..3726b987ec 100644
--- a/released/packages/coq-high-school-geometry/coq-high-school-geometry.8.16.0/opam
+++ b/released/packages/coq-high-school-geometry/coq-high-school-geometry.8.16.0/opam
@@ -15,7 +15,7 @@ Includes a proof of Ptolemy's theorem."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16" & < "8.19"}
+  "coq" {>= "8.16" & < "8.20"}
 ]
 
 tags: [
diff --git a/released/packages/coq-huffman/coq-huffman.8.16.0/opam b/released/packages/coq-huffman/coq-huffman.8.16.0/opam
index 52d26ff8ff..5996298100 100644
--- a/released/packages/coq-huffman/coq-huffman.8.16.0/opam
+++ b/released/packages/coq-huffman/coq-huffman.8.16.0/opam
@@ -16,7 +16,7 @@ Codes, Proc. IRE, pp. 1098-1101, September 1952."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.12" & < "8.19~"}
+  "coq" {>= "8.12" & < "8.20"}
 ]
 
 tags: [
diff --git a/released/packages/coq-jmlcoq/coq-jmlcoq.8.15.0/opam b/released/packages/coq-jmlcoq/coq-jmlcoq.8.15.0/opam
index 09dded3086..652abe7c4e 100644
--- a/released/packages/coq-jmlcoq/coq-jmlcoq.8.15.0/opam
+++ b/released/packages/coq-jmlcoq/coq-jmlcoq.8.15.0/opam
@@ -15,7 +15,7 @@ verified runtime assertion checker for JML."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.10" & < "8.19~"}
+  "coq" {>= "8.10" & < "8.20"}
 ]
 
 tags: [
diff --git a/released/packages/coq-sudoku/coq-sudoku.8.16.0/opam b/released/packages/coq-sudoku/coq-sudoku.8.16.0/opam
index 869c405230..afa4211165 100644
--- a/released/packages/coq-sudoku/coq-sudoku.8.16.0/opam
+++ b/released/packages/coq-sudoku/coq-sudoku.8.16.0/opam
@@ -14,7 +14,7 @@ Davis-Putnam procedure to solve Sudokus."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.12" & < "8.17~"}
+  "coq" {>= "8.12" & < "8.20"}
 ]
 
 tags: [