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 /src/dune | |
| 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 'src/dune')
| -rw-r--r-- | src/dune | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/dune b/src/dune new file mode 100644 index 0000000000..b0140aa809 --- /dev/null +++ b/src/dune @@ -0,0 +1,10 @@ +(library + (name ltac2) + (public_name coq.plugins.ltac2) + (modules_without_implementation tac2expr tac2qexpr tac2types) + (libraries coq.plugins.firstorder)) + +(rule + (targets g_ltac2.ml) + (deps (:pp-file g_ltac2.ml4) ) + (action (run coqp5 -loc loc -impl %{pp-file} -o %{targets}))) |