diff options
| author | Pierre-Marie Pédrot | 2018-11-13 13:46:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-13 13:46:27 +0100 |
| commit | c2f2f5873fca7b60ef5649ec1f1837bbc4ae3084 (patch) | |
| tree | 37c85d78a4b6f534a5d3df02f053d9472cbf567a /grammar/dune | |
| parent | 0b816e4df10d961cce082894f5e4087dc1c95f01 (diff) | |
| parent | 4aa99307874c59f97570f624a06463aaa8115ec5 (diff) | |
Merge PR #8919: [vernac] Rename Vernacinterp to Vernacextend and move extension functions there
Diffstat (limited to 'grammar/dune')
| -rw-r--r-- | grammar/dune | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/grammar/dune b/grammar/dune index f03fe07607..78df2826d6 100644 --- a/grammar/dune +++ b/grammar/dune @@ -1,8 +1,7 @@ (library - (name grammar) + (name grammar5) (synopsis "Coq Camlp5 Grammar Extensions for Plugins") (public_name coq.grammar) - (wrapped false) (flags (:standard -w -58)) (libraries camlp5)) @@ -14,7 +13,7 @@ (rule (targets coqp5) - (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar.cmxa} -o coqp5))) + (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar5.cmxa} -o coqp5))) (install (section bin) |