diff --git a/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/files/future-coercion-class-field.patch b/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/files/future-coercion-class-field.patch
new file mode 100644
index 0000000000..250504bfa8
--- /dev/null
+++ b/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].
diff --git a/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/opam b/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/opam
index 086491eb22..bf79d6646c 100644
--- a/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.0.7.0/opam
+++ b/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: [
diff --git a/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.0.7.0/opam b/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.0.7.0/opam
index 9d26c77976..8555a66368 100644
--- a/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.0.7.0/opam
+++ b/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"