aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cdglobals.mli
Commit message (Expand)AuthorAge
* Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2017-05-30
* Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Gravatar Maxime Dénès2016-07-05
* Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2016-06-29