Merge pull request #3131 from palmskog/analysis-0.7.0-8.20

patch coq-mathcomp-analysis.0.7.0 for Coq 8.20

released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/files/future-coercion-class-field.patch

@@ -0,0 +1,16 @@
+diff --git a/theories/topology.v b/theories/topology.v
+index 4e95029..3bc3d84 100644
+--- a/theories/topology.v
++++ b/theories/topology.v
+@@ -3181,9 +3181,10 @@ Unshelve. all: by end_near. Qed.
+ Section Tychonoff.
+
+ Class UltraFilter T (F : set (set T)) := {
+-  ultra_proper :> ProperFilter F ;
++  ultra_proper : ProperFilter F ;
+   max_filter : forall G : set (set T), ProperFilter G -> F `<=` G -> G = F
+ }.
++#[global] Existing Instance ultra_proper.
+
+ Lemma ultra_cvg_clusterE (T : topologicalType) (F : set (set T)) :
+   UltraFilter F -> cluster F = [set p | F --> p].

released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/opam

@@ -11,6 +11,9 @@ description: """
 This repository contains an experimental library for real analysis for
 the Coq proof-assistant and using the Mathematical Components library."""
 
+patches: [
+  "future-coercion-class-field.patch"
+]
 build: [make "-C" "theories" "-j%{jobs}%"]
 install: [make "-C" "theories" "install"]
 depends: [

released/packages/coq-mathcomp-classical/coq-mathcomp-classical.0.7.0/opam

@@ -14,7 +14,7 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  "coq" { (>= "8.15" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.15" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.20~") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"