From 4f2da48207010b5edca8f0a9a4c5afe7e10eec17 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 27 Apr 2019 15:37:09 +0200
Subject: [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.
---
 META.coq.in                     | 6 +++---
 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))
-- 
cgit v1.2.3