aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto3
AgeCommit message (Collapse)Author
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
This improves error reporting. Addendum to #10515
2019-06-03Update tutorial plugin to use sigma, in keeping with doc recommendationsTalia Ringer
2019-05-21Fixing typos - Part 1JPR
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
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