backwards-compatible patch to make coq-mmaps.1.1 work with Coq 8.20

coq · Aug 11, 2024 · 1a244c8 · 1a244c8
1 parent 654f540
commit 1a244c8
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: [