From 6b30ce5fdfc00ea2b8141b16d765a3459be15e12 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 30 May 2022 14:14:03 +0200
Subject: [PATCH] Adapt to math-comp/math-comp#878

---
 theories/topology.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/topology.v b/theories/topology.v
index b9b181b0f..470bdd66b 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3178,7 +3178,7 @@ Lemma open_hausdorff : hausdorff_space T =
                 [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].
 Proof.
 rewrite propeqE; split => [T_filterT2|T_openT2] x y.
-  have := contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).
+  have := @contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).  (* change @contra_not _ _ to contra_not when requiring MathComp > 1.14 *)
   move=> /[apply] /asboolPn/existsp_asboolPn[A]; rewrite -existsNE => -[B].
   rewrite [nbhs _ _ -> _](rwP imply_asboolP) => /negP.
   rewrite asbool_imply !negb_imply => /andP[/asboolP xA] /andP[/asboolP yB].