blob: a40706e9965d15df3989230c12dbefbe89c01bab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
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.
|
