Merge pull request #3141 from palmskog/mmaps-1.1-8.20

backwards-compatible patch to make coq-mmaps.1.1 work with Coq 8.20
coq · Aug 11, 2024 · 1b47e94 · 1b47e94
2 parents 654f540 + 1a244c8
commit 1b47e94
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 1 deletion.
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
@@ -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
@@ -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: [