diff options
| author | Emilio Jesus Gallego Arias | 2018-10-17 02:02:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-17 02:05:31 +0200 |
| commit | 8b9b1be48a9c83f70cbfb70f52eabc616065fa1e (patch) | |
| tree | edbe6a709cea1379c6a7bad7ef5605e5cfc055ae /doc/plugin_tutorial/tuto1 | |
| parent | 120a8020f6b98ea00988cc37641944811832d139 (diff) | |
[build] Add dune file + fix warnings.
This allows to drop the ltac2 folder inside the Coq dir and have it
compose with the Coq build.
I've fixed build warnings by the way.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions