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.

39 files changed, 130 insertions, 26 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index dab81c8ef6..5a1f92d590 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -161,28 +161,20 @@ let declare_tactic loc s c cl =
   let se = mlexpr_of_string s in
   let pp = make_printing_rule se cl in
   let gl = mlexpr_of_clause cl in
-  let atomic_tactics =
+  let atom =
     mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
       (possibly_atomic loc cl) in
   declare_str_items loc
     [ <:str_item< do {
       try do {
         Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$;
-        List.iter
-          (fun (s,l) -> match l with
-           [ Some l ->
-              Tacenv.register_atomic_ltac (Names.Id.of_string s)
-              (Tacexpr.TacAtom($default_loc$,
-                 Tacexpr.TacExtend($default_loc$,$se$,l)))
-           | None -> () ])
-          $atomic_tactics$ }
+        Mltop.declare_cache_obj (fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ $atom$) __coq_plugin_name;
+        List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; }
       with [ e when Errors.noncritical e ->
 	Pp.msg_warning
 	  (Pp.app
 	     (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
-	     (Errors.print e)) ];
-      Egramcoq.extend_ml_tactic_grammar $se$ $gl$;
-      List.iter (fun (s, r) -> Pptactic.declare_ml_tactic_pprule s r) $pp$; } >>
+	     (Errors.print e)) ]; } >>
     ]
 
 open Pcaml
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 1a25eabe5e..fac81cdceb 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)]);
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index 795211c200..bc5a390027 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool PArith DecidableClass ROmega.
+Require Import Bool PArith DecidableClass Omega ROmega.
 
 Ltac bool :=
 repeat match goal with
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index e31948ffe4..8a95d5b4be 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -1,4 +1,4 @@
-Require Import Bool DecidableClass Algebra Ring PArith ROmega.
+Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega.
 
 Section Bool.
 
diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4
index a45203d3dd..ce99756e01 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+DECLARE PLUGIN "btauto_plugin"
+
 TACTIC EXTEND btauto
 | [ "btauto" ] -> [ Refl_btauto.Btauto.tac ]
 END
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index c2c437c80c..5d6f172c4c 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -10,6 +10,8 @@
 
 open Cctac
 
+DECLARE PLUGIN "cc_plugin"
+
 (* Tactic registration *)
 
 TACTIC EXTEND cc
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 9ae8fcbf67..c3ae05de6a 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -16,6 +16,8 @@ open Tacticals
 open Tacinterp
 open Libnames
 
+DECLARE PLUGIN "ground_plugin"
+
 (* declaring search depth as a global option *)
 
 let ground_depth=ref 3
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 1635cecc08..11107385da 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -10,6 +10,8 @@
 
 open FourierR
 
+DECLARE PLUGIN "fourier_plugin"
+
 TACTIC EXTEND fourier
   [ "fourierz" ] -> [ Proofview.V82.tactic fourier ]
 END
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 90282fcf7b..21d0b9f3db 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -19,6 +19,8 @@ open Genarg
 open Tacticals
 open Misctypes
 
+DECLARE PLUGIN "recdef_plugin"
+
 let pr_binding prc = function
   | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
   | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 78d1e17563..7ed40acb43 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -19,6 +19,8 @@
 open Errors
 open Misctypes
 
+DECLARE PLUGIN "micromega_plugin"
+
 let out_arg = function
   | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 6fd8ab8e9a..20b3ac1e1c 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -17,6 +17,8 @@ open Coqlib
 open Num
 open Utile
 
+DECLARE PLUGIN "nsatz_plugin"
+
 (***********************************************************************
  Operations on coefficients
 *)
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index b384478ae2..83092ccc49 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -15,6 +15,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "omega_plugin"
+
 open Coq_omega
 
 let omega_tactic l =
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 1f11b07ad9..47a62c9e6f 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -14,6 +14,8 @@ open Tacexpr
 open Geninterp
 open Quote
 
+DECLARE PLUGIN "quote_plugin"
+
 let loc = Loc.ghost
 let cont = (loc, Id.of_string "cont")
 let x = (loc, Id.of_string "x")
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index c07825f8cd..4b6c9b7905 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "romega_plugin"
+
 open Refl_omega
 
 let romega_tactic l =
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 7d0b7a1bc1..b908547011 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+DECLARE PLUGIN "rtauto_plugin"
+
 TACTIC EXTEND rtauto
   [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ]
 END
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
index 58a4d7ea65..605a23a987 100644
--- a/plugins/setoid_ring/Rings_Z.v
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -1,6 +1,7 @@
 Require Export Cring.
 Require Export Integral_domain.
 Require Export Ncring_initial.
+Require Export Omega.
 
 Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 8df061870d..8d83ffc330 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -31,6 +31,8 @@ open Decl_kinds
 open Entries
 open Misctypes
 
+DECLARE PLUGIN "newring_plugin"
+
 (****************************************************************************)
 (* controlled reduction *)
 
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
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index d3b65c1746..7cf478e183 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -80,3 +80,12 @@ Delimit Scope core_scope with core.
 
 Open Scope core_scope.
 Open Scope type_scope.
+
+(** ML Tactic Notations *)
+
+Declare ML Module "extratactics".
+Declare ML Module "eauto".
+Declare ML Module "g_class".
+Declare ML Module "g_eqdecide".
+Declare ML Module "g_rewrite".
+Declare ML Module "tauto".
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index c296d427d0..2cfd2790fb 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -12,6 +12,7 @@ Require Import SeqSeries.
 Require Import Rtrigo_def.
 Require Import Cos_rel.
 Require Import Max.
+Require Import Omega.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index 9c7472fe05..335d5b16a1 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -10,6 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo_def.
+Require Import Omega.
 Local Open Scope R_scope.
 
 Definition A1 (x:R) (N:nat) : R :=
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 40064fd511..dbf48e61a7 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -15,6 +15,7 @@ Require Import PSeries_reg.
 Require Import Div2.
 Require Import Even.
 Require Import Max.
+Require Import Omega.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 0166ceda65..311f290987 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -16,6 +16,7 @@ Require Import Rseries.
 Require Import SeqProp.
 Require Import PartSum.
 Require Import Ratan.
+Require Import Omega.
 
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index b2d9c749fd..c66c7b412b 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -9,6 +9,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
+Require Import Omega.
 Local Open Scope R_scope.
 
 (**********)
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index 0614f39982..3a5f932dde 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -14,6 +14,7 @@ Require Import Fourier.
 Require Import RiemannInt.
 Require Import SeqProp.
 Require Import Max.
+Require Import Omega.
 Local Open Scope R_scope.
 
 (** * Preliminaries lemmas *)
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index 45a7032707..dcf2f97095 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -18,6 +18,7 @@ Require Import SeqProp.
 Require Import Ranalysis5.
 Require Import SeqSeries.
 Require Import PartSum.
+Require Import Omega.
 
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 88c4de2390..d5f1994c56 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -12,6 +12,7 @@ Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
 Require Import Binomial.
+Require Import Omega.
 Local Open Scope R_scope.
 
 (** TT Ak; 0<=k<=N *)
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 76b44d9690..ae8074a28c 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -10,6 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
+Require Import Omega.
 Local Open Scope R_scope.
 
 Set Implicit Arguments.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 52657b4015..7f3282a358 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -10,6 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import Max.
+Require Import Omega.
 Local Open Scope R_scope.
 
 (*****************************************************************)
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 995a77ccec..87ffce0b6f 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
+Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega.
 
 Set Implicit Arguments.
 
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index 40d2b1295f..aeddeb70c2 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -23,6 +23,7 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zdiv.
 Require Import Znumtheory.
+Require Import Omega.
 
 Open Scope Z_scope.
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 3b86cf72f8..a64f32d099 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -126,6 +126,51 @@ let add_tactic_notation (local,n,prods,e) =
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)
 
 (**********************************************************************)
+(* ML Tactic entries                                                  *)
+
+type atomic_entry = string * Genarg.glob_generic_argument list option
+
+type ml_tactic_grammar_obj = {
+  mltacobj_name : string;
+  (** ML-side unique name *)
+  mltacobj_prod : grammar_prod_item list list;
+  (** Grammar rules generating the ML tactic. *)
+  mltacobj_atom : atomic_entry list;
+  (** ML tactic notations whose use can be restricted to an identifier. *)
+}
+
+let extend_atomic_tactic name entries =
+  let add_atomic (id, args) = match args with
+  | None -> ()
+  | Some args ->
+    let loc = Loc.ghost in
+    let body = Tacexpr.TacAtom (loc, Tacexpr.TacExtend (loc, name, args)) in
+    Tacenv.register_atomic_ltac (Names.Id.of_string id) body
+  in
+  List.iter add_atomic entries
+
+let cache_ml_tactic_notation (_, obj) =
+  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod;
+  extend_atomic_tactic obj.mltacobj_name obj.mltacobj_atom
+
+let open_ml_tactic_notation i obj =
+  if Int.equal i 1 then cache_ml_tactic_notation obj
+
+let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
+  declare_object { (default_object "MLTacticGrammar") with
+    open_function = open_ml_tactic_notation;
+    cache_function = cache_ml_tactic_notation;
+  }
+
+let add_ml_tactic_notation name prods atomic =
+  let obj = {
+    mltacobj_name = name;
+    mltacobj_prod = prods;
+    mltacobj_atom = atomic;
+  } in
+  Lib.add_anonymous_leaf (inMLTacticGrammar obj)
+
+(**********************************************************************)
 (* Printing grammar entries                                           *)
 
 let entry_buf = Buffer.create 64
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 20326c9c8d..326af7bba2 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -21,6 +21,11 @@ val add_tactic_notation :
   locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr ->
     unit
 
+type atomic_entry = string * Genarg.glob_generic_argument list option
+
+val add_ml_tactic_notation : string ->
+  Egramml.grammar_prod_item list list -> atomic_entry list -> unit
+
 (** Adding a (constr) notation in the environment*)
 
 val add_infix : locality_flag -> (lstring * syntax_modifier list) ->