blob: 65c1e522af7bcfbdd89bb606f24fc62ec1b0f128 (
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
27
28
29
30
31
32
|
How to debug universes?
1. There is a command Dump Universes in Coq toplevel
Dump Universes.
prints the graph of universes in the form of constraints
Dump 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.
*) 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.
|
