aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--META.coq.in6
-rw-r--r--plugins/funind/plugin_base.dune2
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))