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.
---
 parsing/g_ltac.ml4    | 2 --
 parsing/parsing.mllib | 1 -
 2 files changed, 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index faea9baddf..d8620a0f21 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -101,8 +101,6 @@ GEXTEND Gram
       | IDENT "idtac"; l = LIST0 message_token -> TacId l
       | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ];
 	  l = LIST0 message_token -> TacFail (n,l)
-      | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg ->
-	  TacArg (!@loc,TacExternal (!@loc,com,req,la))
       | st = simple_tactic -> st
       | IDENT "constr"; ":"; c = Constr.constr ->
           TacArg(!@loc,ConstrMayEval(ConstrTerm c))
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 500d7dde9f..a0cb831931 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -4,4 +4,3 @@ Lexer
 Pcoq
 Egramml
 Egramcoq
-G_xml
-- 
cgit v1.2.3