diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /dev/doc/universes.txt | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
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. - |