aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Misc.tex
AgeCommit message (Collapse)Author
2018-04-05[Sphinx] Move chapter 30 to new infrastructureMaxime Dénès
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2015-01-29Fix some broken Coq scripts in the reference manual.Guillaume Melquiond
2014-07-23Derive plugin: document new syntax.Arnaud Spiwack
2013-12-06Missing file in commit 1fb883.Arnaud Spiwack
It would seem that I forgot to include the actual documentation in 1fb883. As a result, the reference manual didn't compile due to missing dependencies.