diff --git a/theories/charge.v b/theories/charge.v
index 1fd90eb7b..aae9e443c 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -1364,7 +1364,7 @@ pose AP := A `&` P.
 have mAP : measurable AP by exact: measurableI.
 have muAP_gt0 : 0 < mu AP.
   rewrite lt0e measure_ge0// andbT.
-  apply/eqP/(@contra_not _ _ (nu_mu _ mAP))/eqP; rewrite gt_eqF//.
+  apply/eqP/(contra_not (nu_mu _ mAP))/eqP; rewrite gt_eqF//.
   rewrite (@lt_le_trans _ _ (sigma AP))//.
     rewrite (@lt_le_trans _ _ (sigma A))//; last first.
       rewrite (charge_partition _ _ mP mN)// gee_addl//.
diff --git a/theories/topology.v b/theories/topology.v
index a87aff7eb..5d493bd14 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3554,7 +3554,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).  (* change @contra_not _ _ to contra_not when requiring MathComp > 1.14 *)
+  have := contra_not (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).
   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].