diff options
| author | Théo Zimmermann | 2018-12-02 18:56:04 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-06 12:12:29 +0100 |
| commit | 4031789bd30dabdfad941f6ca3a77862057fae58 (patch) | |
| tree | 5614d6f9dcb9101402b3a218b995ad76073f483e /doc/plugin_tutorial/tuto2/src | |
| parent | c1123f1c05943b8d09245b8fa9d90664344c054d (diff) | |
Document the possibility of declaring a Ltac name_goal.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src')
0 files changed, 0 insertions, 0 deletions