From cac202a99bec5f5ada87ca1182b8546bff535dc1 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 31 Jan 2024 12:11:02 +0100
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18590

---
 theories/topology.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/topology.v b/theories/topology.v
index 03a6ed3ec..b396b257b 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3081,9 +3081,12 @@ Unshelve. all: by end_near. Qed.
 Section Tychonoff.
 
 Class UltraFilter T (F : set_system T) := {
-  ultra_proper :> ProperFilter F ;
+  ultra_proper : ProperFilter F ;
   max_filter : forall G : set_system T, ProperFilter G -> F `<=` G -> G = F
 }.
+(* When requiring Coq >= 8.17, replace the line below with
+  #[global] ultra_proper :: ProperFilter F ; *)
+#[global] Existing Instance ultra_proper.
 
 Lemma ultra_cvg_clusterE (T : topologicalType) (F : set_system T) :
   UltraFilter F -> cluster F = [set p | F --> p].