aboutsummaryrefslogtreecommitdiff
path: root/doc/faq/FAQ.tex
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-09-08 19:17:29 +0200
committerPierre-Marie Pédrot2014-09-08 19:21:08 +0200
commit221f5e5622c866d1dae8e5c5e73156fa3e99ccfc (patch)
tree907542d2a4ede10e71db4210c17011c894491edc /doc/faq/FAQ.tex
parent7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 (diff)
Removing the documentation of the XML plugin.
Diffstat (limited to 'doc/faq/FAQ.tex')
-rw-r--r--doc/faq/FAQ.tex1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index fba210c690..1c28063e68 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -295,7 +295,6 @@ There are graphical user interfaces:
There are documentation and browsing tools:
\begin{description}
-\item[Helm/Mowgli] A rendering, searching and publishing tool.
\item[coq-tex] A tool to insert {\Coq} examples within .tex files.
\item[coqdoc] A documentation tool for \Coq.
\item[coqgraph] A tool to generate a dependency graph from {\Coq} sources.