aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
AgeCommit message (Expand)Author
2019-05-01[comDefinition] Use prepare function from DeclareDef.Emilio Jesus Gallego Arias
2019-03-27[plugin tutorial] Adapt to removal of imperative state.Emilio Jesus Gallego Arias
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-01-08Integrate plugin tutorial after code importGaëtan Gilbert
2019-01-08plugin_tutorial: ignore Coqlib.find_reference deprecation warning.Gaëtan Gilbert
2019-01-08Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e...Gaëtan Gilbert