Adapt to coq/coq#18590

math-comp · Jan 31, 2024 · 0299511 · 0299511
1 parent b4f2663
commit 0299511
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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].