aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-01-19 18:41:47 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-01-19 18:42:50 +0100
commite37201c6ca30e576fce2a548b2a9d2bd5363567f (patch)
treedcfc650c8a2cb24acb17682287ccb6754c5f2d16 /tools/coqdep.ml
parenta532777dcfc59128be2daa7cc74c7881a06f8cb3 (diff)
Fixing coqdep graph printing. The transitive reduction algorithm was bugged.
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 873037d22..8ede756cc 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -275,8 +275,8 @@ struct
let to_remove = to_remove && not (node_equal x a && node_equal y b) in
let to_remove = to_remove && connected_through a b x y graph.dir in
if to_remove then
- let dir = remove_edge x y graph.dir in
- let rev = remove_edge y x graph.rev in
+ let dir = remove_edge a b graph.dir in
+ let rev = remove_edge b a graph.rev in
{ dir; rev; }
else graph
in