aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
AgeCommit message (Collapse)Author
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
Not sure what the right solution is here, but we can improve after the merge.
2019-01-08Add 'doc/plugin_tutorial/' from commit ↵Gaëtan Gilbert
'168a13dab1c9987f592994150997e692d4d7e40b' git-subtree-dir: doc/plugin_tutorial git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7 git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b