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)

9 files changed, 12 insertions, 11 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"
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 7259faecd..36df25cc7 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -28,7 +28,7 @@ open Equality
 open Misctypes
 open Proofview.Notations
 
-DECLARE PLUGIN "extratactics"
+DECLARE PLUGIN "ltac_plugin"
 
 (**********************************************************************)
 (* replace, discriminate, injection, simplify_eq                      *)
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index dfd8e88a9..6145e373b 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -18,7 +18,7 @@ open Pcoq.Constr
 open Pltac
 open Hints
 
-DECLARE PLUGIN "g_auto"
+DECLARE PLUGIN "ltac_plugin"
 
 (* Hint bases *)
 
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 905cfd02a..63451210c 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -13,7 +13,7 @@ open Class_tactics
 open Stdarg
 open Tacarg
 
-DECLARE PLUGIN "g_class"
+DECLARE PLUGIN "ltac_plugin"
 
 (** Options: depth, debug and transparency settings. *)
 
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 570cd4e69..dceefeaa1 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -17,7 +17,7 @@
 open API
 open Eqdecide
 
-DECLARE PLUGIN "g_eqdecide"
+DECLARE PLUGIN "ltac_plugin"
 
 TACTIC EXTEND decide_equality
 | [ "decide" "equality" ] -> [ decideEqualityGoal ]
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index e6ddc5cc1..3e6f42006 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -27,7 +27,7 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pltac
 
-DECLARE PLUGIN "g_rewrite"
+DECLARE PLUGIN "ltac_plugin"
 
 type constr_expr_with_bindings = constr_expr with_bindings
 type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index af1c7149d..12b4c81fc 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -21,7 +21,6 @@ G_auto
 G_class
 Rewrite
 G_rewrite
-Tauto
 G_eqdecide
 G_tactic
 G_ltac
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 5eacb1a95..bb56fd78a 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -13,13 +13,14 @@ open Hipattern
 open Names
 open Geninterp
 open Misctypes
+open Ltac_plugin
 open Tacexpr
 open Tacinterp
 open Util
 open Tacticals.New
 open Proofview.Notations
 
-let tauto_plugin = "tauto"
+let tauto_plugin = "tauto_plugin"
 let () = Mltop.add_known_module tauto_plugin
 
 let assoc_var s ist =
diff --git a/plugins/ltac/tauto_plugin.mlpack b/plugins/ltac/tauto_plugin.mlpack
new file mode 100644
index 000000000..b3618018e
--- /dev/null
+++ b/plugins/ltac/tauto_plugin.mlpack
@@ -0,0 +1 @@
+Tauto