1 files changed, 32 insertions, 0 deletions
diff --git a/dev/universes.txt b/dev/universes.txt
new file mode 100644
index 00000000..65c1e522
--- /dev/null
+++ b/dev/universes.txt
@@ -0,0 +1,32 @@
+How to debug universes?
+
+1. There is a command Dump Universes in Coq toplevel
+
+   Dump Universes.
+     prints the graph of universes in the form of constraints
+
+   Dump Universes "file".
+     produces the "file" containing universe constraints in the form
+       univ1 # univ2 ;
+     where # can be either > >= or =
+     
+   The file produced by the latter command can be transformed using
+   the script univdot to dot format.
+   For example
+
+   univdot file | dot -Tps > file.ps
+
+   produces a graph of universes in ps format. 
+   > arrows are red, >= blue, and = black.
+
+
+   *) for dot see http://www.research.att.com/sw/tools/graphviz/
+
+
+2. There is a printing option
+  
+   Termast.print_universes : bool ref
+
+   which, when set (in ocaml after Drop), makes all pretty-printed
+   Type's annotated with the name of the universe.
+