Adapt to math-comp/math-comp#1246

math-comp · Jul 16, 2024 · bd100b0 · bd100b0
1 parent 319c75b
commit bd100b0
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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 ].