From c2d053c6f38a54e3083c8726eccb3e73942107b7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 21 Jan 2015 00:26:59 +0100
Subject: Embedding the index of the ML tactic entry in the Tacexpr AST.

This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
---
 plugins/setoid_ring/newring.ml4 | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 2f9e8509c2..72ebfae486 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -143,6 +143,10 @@ let closed_term_ast l =
     mltac_plugin = "newring_plugin";
     mltac_tactic = "closed_term";
   } in
+  let tacname = {
+    mltac_name = tacname;
+    mltac_index = 0;
+  } in
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Some(Id.of_string"t")],
   TacML(Loc.ghost,tacname,
-- 
cgit v1.2.3