aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto3/src
AgeCommit message (Expand)Author
2019-03-14Add relevance marks on binders.Gaë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