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.

1 files changed, 1 insertions, 1 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 1a25eabe5..fac81cdce 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -258,7 +258,7 @@ type all_grammar_command =
 
 let add_ml_tactic_entry name prods =
   let entry = weaken_entry Tactic.simple_tactic in
-  let mkact loc l = Tacexpr.TacExtend (loc, name, List.map snd l) in
+  let mkact loc l : raw_atomic_tactic_expr = Tacexpr.TacExtend (loc, name, List.map snd l) in
   let rules = List.map (make_rule mkact) prods in
   synchronize_level_positions ();
   grammar_extend entry None (None ,[(None, None, List.rev rules)]);