Merge pull request #12 from proux01/mc_1246

Adapt to math-comp/math-comp#1246
math-comp · Jul 17, 2024 · 5a5ff27 · 5a5ff27
2 parents ff71b25 + 05d5b4a
commit 5a5ff27
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/bigenough.v b/bigenough.v
@@ -101,7 +101,6 @@ Ltac olddone :=
    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].
 
 Ltac big_enough :=