doc/tools · coq · Tangled

forked from coq/coq

coq doc tools

2 folders · 2 files

Gaëtan Gilbert · rocqdomain.py enforce that every warning has a name · 3w ago

Add `Print Height ident.` command. - Prints the definitional height of a given constant. - Also adds `Print Heights.`, which prints the heights of all the constants in scope.

rocqdomain.py enforce that every warning has a name

Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824 from v8.2 branch].

show_latex_messages

[build] [doc] Build a few more targets hygienically