From 691d62a306fe072f0d91ff665a73c29400adfde4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 11 Sep 2014 11:52:00 +0200
Subject: Removing remaining documentation of the XML plugin.

---
 doc/refman/RefMan-com.tex  |  5 ----
 doc/refman/RefMan-ltac.tex | 64 ----------------------------------------------
 2 files changed, 69 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 926ee986a7..56cf8b06a7 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -172,11 +172,6 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 %
 %  Switch on the debug flag.
 
-\item[{\tt -xml}]\ 
-
-  This option is for use with {\tt coqc}. It tells \Coq\ to export on
-  the standard output the content of the compiled file into XML format.
-
 \item[{\tt -with-geoproof} (yes|no)]\ 
 
   Activate or not special functions for Geoproof within {\CoqIDE} (default is yes).
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index bbcb9251da..2b658b15c2 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -972,70 +972,6 @@ without having to cut manually the proof in smaller lemmas.
 
 \ErrMsg \errindex{Proof is not complete}
 
-\subsubsection[Calling an external tactic]{Calling an external tactic\tacindex{external}
-\index{Ltac!external}}
-
-The tactic {\tt external} runs an executable outside the
-{\Coq} executable. The communication is done via an XML encoding of
-constructions. The syntax of the command is
-
-\begin{quote}
-{\tt external} "\textsl{command}" "\textsl{request}" \nelist{\tacarg}{}
-\end{quote}
-
-The string \textsl{command}, to be interpreted in the default
-execution path of the operating system, is the name of the external
-command. The string \textsl{request} is the name of a request to be
-sent to the external command. Finally the list of tactic arguments
-have to evaluate to terms. An XML tree of the following form is sent
-to the standard input of the external command.
-\medskip
-
-\begin{tabular}{l}
-\texttt{<REQUEST req="}\textsl{request}\texttt{">}\\
-the XML tree of the first argument\\
-{\ldots}\\
-the XML tree of the last argument\\
-\texttt{</REQUEST>}\\
-\end{tabular}
-\medskip
-
-Conversely, the external command must send on its standard output an
-XML tree of the following forms:
-
-\medskip
-\begin{tabular}{l}
-\texttt{<TERM>}\\
-the XML tree of a term\\
-\texttt{</TERM>}\\
-\end{tabular}
-\medskip
-
-\noindent or 
-
-\medskip
-\begin{tabular}{l}
-\texttt{<CALL uri="}\textsl{ltac\_qualified\_ident}\texttt{">}\\
-the XML tree of a first argument\\
-{\ldots}\\
-the XML tree of a last argument\\
-\texttt{</CALL>}\\
-\end{tabular}
-
-\medskip
-\noindent where \textsl{ltac\_qualified\_ident} is the name of a
-defined {\ltac} function and each subsequent XML tree is recursively a
-\texttt{CALL} or a \texttt{TERM} node.
-
-The Document Type Definition (DTD) for terms of the Calculus of
-Inductive Constructions is the one developed as part of the MoWGLI
-European project. It can be found in the file {\tt dev/doc/cic.dtd} of
-the {\Coq} source archive.
-
-An example of parser for this DTD, written in the {\ocaml} -
-Camlp4 language, can be found in the file {\tt parsing/g\_xml.ml4} of
-the {\Coq} source archive.
-
 \section[Tactic toplevel definitions]{Tactic toplevel definitions\comindex{Ltac}}
 
 \subsection{Defining {\ltac} functions}
-- 
cgit v1.2.3