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.
---
 printing/pptactic.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 890e0d585b..b6b8c9c2e7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -985,9 +985,6 @@ and pr_tacarg = function
   | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
   | TacPretype c -> str "type_term" ++ pr.pr_constr c
   | TacNumgoals -> str "numgoals"
-  | TacExternal (_,com,req,la) ->
-      str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++
-      spc() ++ prlist_with_sep spc pr_tacarg la
   | (TacCall _|Tacexp _ | TacGeneric _) as a ->
       str "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a))
 
-- 
cgit v1.2.3