Merge pull request #41 from coq-community/mc_1240

Adapt to mathc-omp/math-comp#1240
coq-community · Jul 16, 2024 · aa4e6cb · aa4e6cb
2 parents 4bc2960 + abeb7a9
commit aa4e6cb
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/theories/core/edone.v b/theories/core/edone.v
@@ -24,7 +24,6 @@ Ltac done := trivial; hnf in |- *; intros;
       | apply/andP;split
       | rewrite ?andbT ?andbF ?orbT ?orbF ]
     )
-    | case not_locked_false_eq_true; assumption
     | match goal with
         | H:~ _ |- _ => solve [ case H; trivial ]
       end