aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1/src/simple_declare.ml
AgeCommit message (Expand)Author
2019-10-25[declare] Generalize kind type on declareDefEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-06Clean, document, and expand plugin tutorials 0 and 1Talia Ringer
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
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-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-01-08Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e...Gaëtan Gilbert