diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /dev/doc/universes.txt | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'dev/doc/universes.txt')
-rw-r--r-- | dev/doc/universes.txt | 24 |
1 files changed, 9 insertions, 15 deletions
diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt index 65c1e522..a40706e9 100644 --- a/dev/doc/universes.txt +++ b/dev/doc/universes.txt @@ -1,32 +1,26 @@ How to debug universes? -1. There is a command Dump Universes in Coq toplevel +1. There is a command Print Universes in Coq toplevel - Dump Universes. + Print Universes. prints the graph of universes in the form of constraints - Dump Universes "file". + Print 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. + If "file" ends with .gv or .dot, the resulting file will be in + dot format. *) 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. + {Set,Unset} Printing Universes. + + which, when set, makes all pretty-printed Type's annotated with the + name of the universe. |