diff options
| author | Pierre-Marie Pédrot | 2020-04-09 15:57:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-07 00:22:11 +0200 |
| commit | f694d42400593d7ef3ad6c2812395f941cc4f5ca (patch) | |
| tree | 622217abdb611b4e1dce9d90f827c37dded5581d /doc/plugin_tutorial/Makefile | |
| parent | 325a644b3f5a5f8c1a86191004576e7c763ae9f3 (diff) | |
Add helper API to define low-level Ltac functions.
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions