Skip to content

Commit

Permalink
Merge pull request coq#86 from ejgallego/more-dune
Browse files Browse the repository at this point in the history
[dune] Full Dune support.
  • Loading branch information
ppedrot authored Mar 30, 2019
2 parents bffea0d + f9da21c commit b8a393c
Show file tree
Hide file tree
Showing 6 changed files with 18 additions and 3 deletions.
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,6 @@ Makefile.coq.conf
*.a
*.aux
tests/*.log
*.install
_build
.merlin
3 changes: 3 additions & 0 deletions dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
(env
(dev (flags :standard -rectypes))
(release (flags :standard -rectypes)))
3 changes: 3 additions & 0 deletions dune-project
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
(lang dune 1.6)
(using coq 0.1)
(name ltac2)
Empty file added ltac2.opam
Empty file.
6 changes: 3 additions & 3 deletions src/dune
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
(library
(name ltac2)
(public_name coq.plugins.ltac2)
(name ltac2_plugin)
(public_name ltac2.plugin)
(modules_without_implementation tac2expr tac2qexpr tac2types)
(flags :standard -w -50)
(flags :standard -warn-error -9-27-50)
(libraries coq.plugins.firstorder))

(rule
Expand Down
6 changes: 6 additions & 0 deletions theories/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(coqlib
(name Ltac2) ; This determines the -R flag
(public_name ltac2.Ltac2)
(synopsis "Ltac 2 Plugin")
(libraries ltac2.plugin))

0 comments on commit b8a393c

Please sign in to comment.