adapt to mc#1300

coq-community · Nov 27, 2024 · 5298318 · 5298318
1 parent 2a45b55
commit 5298318
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/kosaraju.v b/theories/kosaraju.v
@@ -738,7 +738,7 @@ have: tsorted r (predT : pred T) [seq i <- tseq (rgraph r) | i \in p.1].
   move=> [tsub tconn tbef] _; split => // x y xtseq.
     by move => xyconn; apply (tconn _ _ xtseq); rewrite -(eq_connect reltoE).
   rewrite (eq_connect reltoE) => conn0; move: (tbef _ _ xtseq conn0).
-  by rewrite /before /= /can_to (eq_find (eq_symconnect reltoE _)).
+  by rewrite /before /= /can_to (eq_find (@eq_symconnect _ _ _ reltoE _)).
 elim: tseq p => [[s l]/= HR HI HE HFI HUF|].
   split=> // i.
   by have := HFI i; rewrite cats0.