plugins/ltac : avoid spurious .cmxs files

 In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
 (for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
  - wrong -for-pack used for their inner .cmx
  - dependency over modules not provided (for instance Tacenv, that ends
    up being a submodule of the pack ltac_plugin).
 But we were lucky, those files were actually never loaded, thanks to the
 several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
 and hence tell Coq that these modules are already known, preventing
 any attempt to load them.

 Anyway, this commit cleans up this mess (thanks PMP for the help)

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 07b8746fb..50013f558 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -17,7 +17,7 @@ open Stdarg
 open Extraargs
 open Names
 
-DECLARE PLUGIN "coretactics"
+DECLARE PLUGIN "ltac_plugin"
 
 (** Basic tactics *)
 
@@ -324,11 +324,11 @@ let initial_atomic () =
         "fresh", TacArg(Loc.tag @@ TacFreshId [])
       ]
 
-let () = Mltop.declare_cache_obj initial_atomic "coretactics"
+let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin"
 
 (* First-class Ltac access to primitive blocks *)
 
-let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; }
+let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; }
 let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
 
 let register_list_tactical name f =
@@ -356,4 +356,4 @@ let initial_tacticals () =
     "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
   ]
 
-let () = Mltop.declare_cache_obj initial_tacticals "coretactics"
+let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"