From b52dca14d3ac66ecd1657a21fecd0b48751096a7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Jul 2014 14:58:03 +0200
Subject: Qualified ML tactic names. The plugin name is used to discriminate
 potentially conflicting tactics names from different plugins.

---
 intf/tacexpr.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 609ee2f369..1375552c32 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -83,6 +83,11 @@ type ('a,'t) match_rule =
   | Pat of 'a match_context_hyps list * 'a match_pattern * 't
   | All of 't
 
+type ml_tactic_name = {
+  mltac_plugin : string;
+  mltac_tactic : string;
+}
+
 (** Composite types *)
 
 (** In globalize tactics, we need to keep the initial [constr_expr] to recompute
@@ -157,7 +162,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
   | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
 
   (* For ML extensions *)
-  | TacExtend of Loc.t * string * 'lev generic_argument list
+  | TacExtend of Loc.t * ml_tactic_name * 'lev generic_argument list
 
   (* For syntax extensions *)
   | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list
-- 
cgit v1.2.3