Adapt to math-comp/math-comp#878

math-comp · Jun 1, 2022 · 6b30ce5 · 6b30ce5
1 parent 82e29a0
commit 6b30ce5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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].