From bd100b06b1324350450ce7a65370a96157988acf Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 15 Jul 2024 18:12:05 +0200
Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1246

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

diff --git a/theories/topology.v b/theories/topology.v
index a9230bead..eb7c846cb 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -954,7 +954,6 @@ Ltac done :=
   trivial; hnf; intros; solve
    [ do ![solve [trivial | apply: sym_equal; trivial]
          | discriminate | contradiction | split]
-   | case not_locked_false_eq_true; assumption
    | match goal with H : ~ _ |- _ => solve [case H; trivial] end
    | match goal with |- ?x \is_near _ => near: x; apply: prop_ofP end ].