diff options
| author | Emilio Jesus Gallego Arias | 2018-11-06 14:25:33 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-13 12:11:47 +0100 |
| commit | 4aa99307874c59f97570f624a06463aaa8115ec5 (patch) | |
| tree | 37c85d78a4b6f534a5d3df02f053d9472cbf567a /grammar/dune | |
| parent | 76048d675212211b623616da7132826d1ee41870 (diff) | |
[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.
This PR fixes an issues that was bugging me for some time, namely that
`Vernacinterp` really means `Vernacextend`.
We thus rename the file and move the associated functions there, which
were incorrectly placed in `Vernacentries`.
Note the beneficial effects on reducing the `.mli` API.
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) |