diff options
| author | Emilio Jesus Gallego Arias | 2019-04-27 15:37:09 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-29 07:11:04 +0000 |
| commit | 4f2da48207010b5edca8f0a9a4c5afe7e10eec17 (patch) | |
| tree | 264d39a9a8bbe69ff98d7c7c7038d6972d2e2ad8 /plugins/funind/plugin_base.dune | |
| parent | f1fd3d42d87f8b9dd840c613dad235e3b5f3338e (diff) | |
[meta] [dune] Fix discrepancies in plugin names
We have some discrepancy with the package names for plugins in the
META / Dune case. This PR fixes it.
At some point there was a need for plugin package names having to be
named as their directories.
I think this is not true anymore, but taking the "dir_name ==
package_name" convention just in case.
Diffstat (limited to 'plugins/funind/plugin_base.dune')
| -rw-r--r-- | plugins/funind/plugin_base.dune | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune index 002eb28eea..6ccf15df29 100644 --- a/plugins/funind/plugin_base.dune +++ b/plugins/funind/plugin_base.dune @@ -1,5 +1,5 @@ (library (name recdef_plugin) - (public_name coq.plugins.recdef) + (public_name coq.plugins.funind) (synopsis "Coq's functional induction plugin") (libraries coq.plugins.extraction)) |