aboutsummaryrefslogtreecommitdiff
path: root/tools/coqdoc/cdglobals.mli
AgeCommit message (Expand)Author
2017-05-30Makefile: no bytecode compilation in make world, see make byte insteadPierre Letouzey
2016-07-05Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Maxime Dénès
2016-06-29Makefile: no bytecode compilation in make world, see make byte insteadPierre Letouzey