I am now using tred to remove transitive dependencies from the graph before

displaying it.

diff --git a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
index d857ab93e1f1f22d77c46786aa1f258cf57ec611..3a9dcde307c90260b146bb5aec7f3c1735e6f2ff 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
+++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml
@@ -99,7 +99,7 @@ let ps_of_set (to_be_considered,under_consideration,news) ?processing s =
           "style=dashed];\n"));
   output_string ch "}\n";
   close_out ch;
-  ignore (Unix.system "dot -Tps xxx.dot > xxx.ps")
+  ignore (Unix.system "tred xxx.dot > yyy.dot && dot -Tps yyy.dot > xxx.ps")
 
 let test to_be_considered_and_now set rel candidate repr =
  ps_of_set to_be_considered_and_now ~processing:(candidate,rel,repr) set;