From ee162ba3b28fccca0a2b3ea4b1e0811006840570 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 24 Feb 2016 10:07:57 +0100
Subject: Removing the MetaIdArg entry of tactic expressions.

This was historically used together with the <:tactic< ... >> quotation to insert
foreign code as $foo, but it actually only survived in the implementation of Tauto.
With the removal of the quotation feature, this is now totally obsolete.
---
 intf/tacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 57c61874a..502f2db4c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -206,7 +206,6 @@ constraint 'a = <
 
 and 'a gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
-  | MetaIdArg      of Loc.t * bool * string
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
   | UConstr        of 'utrm
   | Reference      of 'ref
-- 
cgit v1.2.3