aboutsummaryrefslogtreecommitdiff
path: root/grammar/vernacextend.mlp
AgeCommit message (Expand)Author
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-05-30make the expansion of the "DECLARE PLUGIN" closer to the way how a human woul...Matej Kosik
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-16Adding support for using grammar entries returning no value in EXTEND.Hugo Herbelin
2017-04-25[location] Remove `Loc.internal_ghost`Emilio Jesus Gallego Arias
2017-04-14Fix compilation with camlp5 transitional mode.Maxime Dénès
2017-04-07[camlpX] Remove camlp4 compat layer.Emilio Jesus Gallego Arias
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-01Merge branch 'yet-another-makefile-bigbang' into trunkPierre Letouzey
2016-06-01Yet another Makefile reform : a unique phase without nasty make tricksPierre Letouzey