From 1a244c80634cda402ef26d7c0d239f7085298d91 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sun, 11 Aug 2024 12:04:10 +0200
Subject: [PATCH] backwards-compatible patch to make coq-mmaps.1.1 work with
 Coq 8.20

---
 .../files/class-field-instance.patch              | 15 +++++++++++++++
 released/packages/coq-mmaps/coq-mmaps.1.1/opam    |  3 ++-
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 released/packages/coq-mmaps/coq-mmaps.1.1/files/class-field-instance.patch

diff --git a/released/packages/coq-mmaps/coq-mmaps.1.1/files/class-field-instance.patch b/released/packages/coq-mmaps/coq-mmaps.1.1/files/class-field-instance.patch
new file mode 100644
index 0000000000..c2582b9ffb
--- /dev/null
+++ b/released/packages/coq-mmaps/coq-mmaps.1.1/files/class-field-instance.patch
@@ -0,0 +1,15 @@
+diff --git a/theories/Comparisons.v b/theories/Comparisons.v
+index bb3950e..50b6a0f 100644
+--- a/theories/Comparisons.v
++++ b/theories/Comparisons.v
+@@ -25,8 +25,8 @@ Definition Trans {A} (cmp:A->A->comparison) :=
+   forall c x y z, cmp x y = c -> cmp y z = c -> cmp x z = c.
+ 
+ Class SymTrans {A} (cmp:A->A->comparison) := {
+-  sym :> Sym cmp;
+-  tra :> Trans cmp
++  sym : Sym cmp;
++  tra : Trans cmp
+ }.
+ 
+ (** [SymTrans] implies the following compatibility rules *)
diff --git a/released/packages/coq-mmaps/coq-mmaps.1.1/opam b/released/packages/coq-mmaps/coq-mmaps.1.1/opam
index 741ad12537..69d79b3979 100644
--- a/released/packages/coq-mmaps/coq-mmaps.1.1/opam
+++ b/released/packages/coq-mmaps/coq-mmaps.1.1/opam
@@ -14,10 +14,11 @@ The finite maps are parameterized on arbitrary ordered types using
 Coq functors. This is an updated version of the Coq Stdlib's FMaps
 that is meant to complement the Stdlib's MSet library."""
 
+patches: ["class-field-instance.patch"]
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.14" & < "8.20"}
+  "coq" {>= "8.14" & < "8.21"}
 ]
 
 tags: [