aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-08 18:34:04 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-08 18:46:25 +0200
commit7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 (patch)
treeeeb9435bb4e64566647c5626a2a0f4b83eb58b08 /parsing
parent7a5eb53973ec3fd921b56339557c48681972849e (diff)
Removing the XML plugin.
Left a README, just in case someone will discover the remnants of it decades from now.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_ltac.ml42
-rw-r--r--parsing/parsing.mllib1
2 files changed, 0 insertions, 3 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index faea9badd..d8620a0f2 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 500d7dde9..a0cb83193 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -4,4 +4,3 @@ Lexer
Pcoq
Egramml
Egramcoq
-G_xml