Now parsing rules of ML-declared tactics are only made available after the

corresponding Declare ML Module command. This changes essentially two
things:

1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.

2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.

7 files changed, 27 insertions, 10 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 96258a84bc..4674bd030c 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -28,6 +28,8 @@ open Misctypes
 open Locus
 open Locusops
 
+DECLARE PLUGIN "eauto"
+
 let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
 
 let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e87c665d09..f6483e2b3d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -22,6 +22,8 @@ open Evd
 open Equality
 open Misctypes
 
+DECLARE PLUGIN "extratactics"
+
 (**********************************************************************)
 (* admit, replace, discriminate, injection, simplify_eq               *)
 (* cutrewrite, dependent rewrite                                      *)
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index 6012088f7b..1e666e5a55 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -11,6 +11,8 @@
 open Misctypes
 open Class_tactics
 
+DECLARE PLUGIN "g_class"
+
 TACTIC EXTEND progress_evars
   [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ]
 END
diff --git a/tactics/g_eqdecide.ml4 b/tactics/g_eqdecide.ml4
index c9d876d92f..819bbdc518 100644
--- a/tactics/g_eqdecide.ml4
+++ b/tactics/g_eqdecide.ml4
@@ -16,6 +16,8 @@
 
 open Eqdecide
 
+DECLARE PLUGIN "g_eqdecide"
+
 TACTIC EXTEND decide_equality
 | [ "decide" "equality" ] -> [ decideEqualityGoal ]
 END
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 779070f80a..27233ea57b 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -21,6 +21,8 @@ open Tacmach
 open Tacticals
 open Rewrite
 
+DECLARE PLUGIN "g_rewrite"
+
 type constr_expr_with_bindings = constr_expr with_bindings
 type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
 type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 9bd3128546..9259048260 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -59,19 +59,18 @@ let () =
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
-let atomic_mactab = ref Id.Map.empty
 
-let register_atomic_ltac id tac =
-  atomic_mactab := Id.Map.add id tac !atomic_mactab
-
-let _ =
+let initial_atomic =
   let open Locus in
   let open Misctypes in
   let open Genredexpr in
   let dloc = Loc.ghost in
   let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
-  List.iter
-      (fun (s,t) -> register_atomic_ltac (Id.of_string s) (TacAtom(dloc,t)))
+  let fold accu (s, t) =
+    let body = TacAtom (dloc, t) in
+    Id.Map.add (Id.of_string s) body accu
+  in
+  let ans = List.fold_left fold Id.Map.empty
       [ "red", TacReduce(Red false,nocl);
         "hnf", TacReduce(Hnf,nocl);
         "simpl", TacReduce(Simpl None,nocl);
@@ -92,14 +91,20 @@ let _ =
         "econstructor", TacAnyConstructor (true,None);
         "reflexivity", TacReflexivity;
         "symmetry", TacSymmetry nocl
-      ];
-  List.iter
-      (fun (s,t) -> register_atomic_ltac (Id.of_string s) t)
+      ]
+  in
+  let fold accu (s, t) = Id.Map.add (Id.of_string s) t accu in
+  List.fold_left fold ans
       [ "idtac",TacId [];
         "fail", TacFail(ArgArg 0,[]);
         "fresh", TacArg(dloc,TacFreshId [])
       ]
 
+let atomic_mactab = Summary.ref ~name:"atomic_tactics" initial_atomic
+
+let register_atomic_ltac id tac =
+  atomic_mactab := Id.Map.add id tac !atomic_mactab
+
 let interp_atomic_ltac id = Id.Map.find id !atomic_mactab
 
 let is_primitive_ltac_ident id =
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 8d3d335102..2d9b4da967 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -20,6 +20,8 @@ open Tactics
 open Errors
 open Util
 
+DECLARE PLUGIN "tauto"
+
 let assoc_var s ist =
   let v = Id.Map.find (Names.Id.of_string s) ist.lfun in
   match Value.to_constr v with