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 | |
| 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.
| -rw-r--r-- | META.coq.in | 6 | ||||
| -rw-r--r-- | plugins/funind/plugin_base.dune | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/META.coq.in b/META.coq.in index ab142ccc43..ef5de8da2b 100644 --- a/META.coq.in +++ b/META.coq.in @@ -315,7 +315,7 @@ package "plugins" ( archive(native) = "micromega_plugin.cmx" ) - package "newring" ( + package "setoid_ring" ( description = "Coq newring plugin" version = "8.10" @@ -351,7 +351,7 @@ package "plugins" ( archive(native) = "cc_plugin.cmx" ) - package "ground" ( + package "firstorder" ( description = "Coq ground plugin" version = "8.10" @@ -387,7 +387,7 @@ package "plugins" ( archive(native) = "btauto_plugin.cmx" ) - package "recdef" ( + package "funind" ( description = "Coq recdef plugin" version = "8.10" 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)) |