From 52983181d450b07570badf83142ab598219f541a Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Wed, 27 Nov 2024 17:26:59 +0100
Subject: [PATCH] adapt to mc#1300

---
 theories/kosaraju.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/kosaraju.v b/theories/kosaraju.v
index de52e2f..c27fc7f 100644
--- 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.