aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/practical-tools
ModeNameSize
-rw-r--r--coq-commands.rst13541logplain
-rw-r--r--coqide.rst13362logplain
-rw-r--r--utilities.rst32227logplain