Adapt to math-comp/math-comp#1046

coq-community · Nov 22, 2023 · 4f16eda · 4f16eda
1 parent bc1161b
commit 4f16eda
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/theories/two_way.v b/theories/two_way.v
@@ -130,7 +130,8 @@ Section DFA2.
   Proof.
     rewrite /read.
     case: (ord2P _) => [||i] _;apply cards_lt1; rewrite ?cardsX ?cards1 ?muln1;
-      by auto using detL, detC, detR, dfa2_det.
+      [auto using detL, detC, detR, dfa2_det..|].
+    exact/detC/dfa2_det.
   Qed.
 
   Lemma step_fun x : functional (step M x).