diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /dev/doc/universes.txt | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
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. |