From 7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Sep 2014 18:34:04 +0200
Subject: Removing the XML plugin.

Left a README, just in case someone will discover the remnants of it
decades from now.
---
 intf/tacexpr.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e2995cfabc..55d6e53a51 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -185,8 +185,6 @@ and ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg =
   | Reference      of 'ref
   | TacCall of Loc.t * 'ref *
       ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list
-  | TacExternal of Loc.t * string * string *
-      ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list
   | TacFreshId of string or_var list
   | Tacexp of ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr
   | TacPretype of 'trm
-- 
cgit v1.2.3