diff options
Diffstat (limited to 'dev/doc/universes.txt')
| -rw-r--r-- | dev/doc/universes.txt | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt deleted file mode 100644 index a40706e9..00000000 --- a/dev/doc/universes.txt +++ /dev/null @@ -1,26 +0,0 @@ -How to debug universes? - -1. There is a command Print Universes in Coq toplevel - - Print Universes. - prints the graph of universes in the form of constraints - - Print Universes "file". - produces the "file" containing universe constraints in the form - univ1 # univ2 ; - where # can be either > >= or = - - 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 - - {Set,Unset} Printing Universes. - - which, when set, makes all pretty-printed Type's annotated with the - name of the universe. - |