From d1d511b6b65109ed561ab158d0b231f399d4c01c Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 20 Mar 2019 00:13:33 +0100
Subject: [doc] Mention that fingraph's connect computes the reflexive
 transitive closure

while some refs (see e.g. [1]) don't assume that the "transitive closure" is
reflexive; so one won't need to look at lemma "connect0" to figure this out.

[1] https://en.wikipedia.org/wiki/Transitive_closure

[ci skip]
---
 mathcomp/ssreflect/fingraph.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 5358dc7..1a0f25f 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -14,7 +14,7 @@ Require Import ssrbool ssrfun eqtype ssrnat seq path fintype.
 (*    dfs g n v x == the list of points traversed by a depth-first search of  *)
 (*                   the g, at depth n, starting from x, and avoiding v.      *)
 (* dfs_path g v x y <-> there is a path from x to y in g \ v.                 *)
-(*      connect e == the transitive closure of e (computed by dfs).           *)
+(*      connect e == the reflexive transitive closure of e (computed by dfs). *)
 (*  connect_sym e <-> connect e is symmetric, hence an equivalence relation.  *)
 (*       root e x == a representative of connect e x, which is the component  *)
 (*                   of x in the transitive closure of e.                     *)
-- 
cgit v1.2.3