aboutsummaryrefslogtreecommitdiff
path: root/coqpp/dune
diff options
context:
space:
mode:
authorThéo Zimmermann2019-07-20 12:50:17 +0200
committerThéo Zimmermann2019-07-20 12:50:17 +0200
commitcd6fc50854285f02bf151e94bdfb819988531fd2 (patch)
tree798fcfd6a0bd529a3d8ae8a25e1c1e62b728be26 /coqpp/dune
parentc80dfb6bd8ff8625ced2cae8b6789707f904a118 (diff)
parentcf868740c3d18ee9ce9a6b38dd617784625a3cae (diff)
Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg files and insert it into .rst files
Ack-by: Zimmi48 Ack-by: gares Ack-by: ppedrot
Diffstat (limited to 'coqpp/dune')
-rw-r--r--coqpp/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/coqpp/dune b/coqpp/dune
index a6edf4cf5b..12071c7c05 100644
--- a/coqpp/dune
+++ b/coqpp/dune
@@ -5,5 +5,5 @@
(name coqpp_main)
(public_name coqpp)
(package coq)
- (modules coqpp_ast coqpp_lex coqpp_parse coqpp_main)
+ (modules coqpp_ast coqpp_lex coqpp_parse coqpp_parser coqpp_main)
(modules_without_implementation coqpp_ast))