aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-28 17:31:03 +0200
committerEmilio Jesus Gallego Arias2018-09-28 17:36:49 +0200
commit834bd20dc5d6024933e7f859ad5e697fc8b27b9d (patch)
tree4e3a7819dc1697316053d883ac9d4e09af2eac45 /checker
parent0bcbc990dcebce2e66f10aba462c9fed2c2eda06 (diff)
[dune] Pack checker to avoid [odoc] problems + build doc for plugins.
We also build documentation for plugins, for example Ltac_plugin is often used in other plugins.
Diffstat (limited to 'checker')
-rw-r--r--checker/dune22
1 files changed, 14 insertions, 8 deletions
diff --git a/checker/dune b/checker/dune
index d918f853dd..d520171f98 100644
--- a/checker/dune
+++ b/checker/dune
@@ -3,24 +3,30 @@
(rule (copy %{project_root}/kernel/esubst.ml esubst.ml))
(rule (copy %{project_root}/kernel/esubst.mli esubst.mli))
+; Careful with bug https://github.com/ocaml/odoc/issues/148
+;
+; If we don't pack checker we will have a problem here due to
+; duplicate module names in the whole build.
(library
- (name checker)
- (public_name coq.checker)
+ (name checklib)
+ (public_name coq.checklib)
(synopsis "Coq's Standalone Proof Checker")
- (modules values analyze names esubst)
- (wrapped false)
+ (modules :standard \ main votour)
+ (modules_without_implementation cic)
+ (wrapped true)
(libraries coq.lib))
(executable
(name main)
(public_name coqchk)
- (modules :standard \ votour values analyze names esubst)
- (modules_without_implementation cic)
- (libraries coq.checker))
+ (modules main)
+ (flags :standard -open Checklib)
+ (libraries coq.checklib))
(executable
(name votour)
(public_name votour)
(modules votour)
- (libraries coq.checker))
+ (flags :standard -open Checklib)
+ (libraries coq.checklib))