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.

---
 plugins/setoid_ring/newring.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 8d83ffc330..18be9b2282 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -139,9 +139,13 @@ let closed_term_ast l =
    Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
 *)
 let closed_term_ast l =
+  let tacname = {
+    mltac_plugin = "newring_plugin";
+    mltac_tactic = "closed_term";
+  } in
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
-  TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
+  TacAtom(Loc.ghost,TacExtend(Loc.ghost,tacname,
   [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
    Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])))
 (*
-- 
cgit v1.2.3