Remove the part about coqdoc from the utilities chapter.

(It was moved out onto a separate page.)

1 files changed, 0 insertions, 464 deletions

diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e5ff26520a..d61e5ddce7 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -637,470 +637,6 @@ See the man page of ``coqdep`` for more details and options.
 Both Dune and ``coq_makefile`` use ``coqdep`` to compute the
 dependencies among the files part of a Coq project.
 
-.. _coqdoc:
-
-Documenting |Coq| files with coqdoc
------------------------------------
-
-coqdoc is a documentation tool for the proof assistant |Coq|, similar to
-``javadoc`` or ``ocamldoc``. The task of coqdoc is
-
-
-#. to produce a nice |Latex| and/or HTML document from |Coq| source files,
-   readable for a human and not only for the proof assistant;
-#. to help the user navigate his own (or third-party) sources.
-
-
-
-Principles
-~~~~~~~~~~
-
-Documentation is inserted into |Coq| files as *special comments*. Thus
-your files will compile as usual, whether you use coqdoc or not. coqdoc
-presupposes that the given |Coq| files are well-formed (at least
-lexically). Documentation starts with ``(**``, followed by a space, and
-ends with ``*)``. The documentation format is inspired by Todd
-A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with
-some syntax-light controls, described below. coqdoc is robust: it
-shouldn’t fail, whatever the input is. But remember: “garbage in,
-garbage out”.
-
-
-|Coq| material inside documentation.
-++++++++++++++++++++++++++++++++++++
-
-|Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets
-may be nested, the inner ones being understood as being part of the
-quoted code (thus you can quote a term like ``fun x => u`` by writing  ``[fun
-x => u]``). Inside quotations, the code is pretty-printed in the same
-way as it is in code parts.
-
-Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be
-followed by a newline and the latter must follow a newline.
-
-
-Pretty-printing.
-++++++++++++++++
-
-coqdoc uses different faces for identifiers and keywords. The pretty-
-printing of |Coq| tokens (identifiers or symbols) can be controlled
-using one of the following commands:
-
-::
-
-
-    (** printing  *token* %...LATEX...% #...html...# *)
-
-
-or
-
-::
-
-
-    (** printing  *token* $...LATEX math...$ #...html...# *)
-
-
-It gives the |Latex| and HTML texts to be produced for the given |Coq|
-token. Either the |Latex| or the HTML rule may be omitted, causing the
-default pretty-printing to be used for this token.
-
-The printing for one token can be removed with
-
-::
-
-
-    (** remove printing  *token* *)
-
-
-Initially, the pretty-printing table contains the following mapping:
-
-===== === ==== ===== === ==== ==== ===
-`->`   →       `<-`   ←       `*`   ×
-`<=`   ≤       `>=`   ≥       `=>`  ⇒
-`<>`   ≠       `<->`  ↔       `|-`  ⊢
-`\\/`  ∨       `/\\`  ∧       `~`   ¬
-===== === ==== ===== === ==== ==== ===
-
-Any of these can be overwritten or suppressed using the printing
-commands.
-
-.. note::
-
-   The recognition of tokens is done by a (``ocaml``) lex
-   automaton and thus applies the longest-match rule. For instance, `->~`
-   is recognized as a single token, where |Coq| sees two tokens. It is the
-   responsibility of the user to insert space between tokens *or* to give
-   pretty-printing rules for the possible combinations, e.g.
-
-   ::
-
-      (** printing ->~ %\ensuremath{\rightarrow\lnot}% *)
-
-
-
-Sections
-++++++++
-
-Sections are introduced by 1 to 4 asterisks at the beginning of a line
-followed by a space and the title of the section. One asterisk is a section,
-two a subsection, etc.
-
-.. example::
-
-   ::
-
-          (** * Well-founded relations
-
-              In this section, we introduce...  *)
-
-
-Lists.
-++++++
-
-List items are introduced by a leading dash. coqdoc uses whitespace to
-determine the depth of a new list item and which text belongs in which
-list items. A list ends when a line of text starts at or before the
-level of indenting of the list’s dash. A list item’s dash must always
-be the first non-space character on its line (so, in particular, a
-list can not begin on the first line of a comment - start it on the
-second line instead).
-
-.. example::
-
-  ::
-
-           We go by induction on [n]:
-           - If [n] is 0...
-           - If [n] is [S n'] we require...
-
-             two paragraphs of reasoning, and two subcases:
-
-             - In the first case...
-             - In the second case...
-
-           So the theorem holds.
-
-
-
-Rules.
-++++++
-
-More than 4 leading dashes produce a horizontal rule.
-
-
-Emphasis.
-+++++++++
-
-Text can be italicized by enclosing it in underscores. A non-identifier
-character must precede the leading underscore and follow the trailing
-underscore, so that uses of underscores in names aren’t mistaken for
-emphasis. Usually, these are spaces or punctuation.
-
-::
-
-        This sentence contains some _emphasized text_.
-
-
-
-Escaping to |Latex| and HTML.
-+++++++++++++++++++++++++++++++
-
-Pure |Latex| or HTML material can be inserted using the following
-escape sequences:
-
-
-+ ``$...LATEX stuff...$`` inserts some |Latex| material in math mode.
-  Simply discarded in HTML output.
-+ ``%...LATEX stuff...%`` inserts some |Latex| material. Simply
-  discarded in HTML output.
-+ ``#...HTML stuff...#`` inserts some HTML material. Simply discarded in
-  |Latex| output.
-
-.. note::
-  to simply output the characters ``$``, ``%`` and ``#`` and escaping
-  their escaping role, these characters must be doubled.
-
-
-Verbatim
-++++++++
-
-Verbatim material is introduced by a leading ``<<`` and closed by ``>>``
-at the beginning of a line.
-
-.. example::
-
-  ::
-
-      Here is the corresponding caml code:
-      <<
-        let rec fact n =
-          if n <= 1 then 1 else n * fact (n-1)
-      >>
-
-
-
-Hyperlinks
-++++++++++
-
-Hyperlinks can be inserted into the HTML output, so that any
-identifier is linked to the place of its definition.
-
-``coqc file.v`` automatically dumps localization information in
-``file.glob`` or appends it to a file specified using the option ``--dump-glob
-file``. Take care of erasing this global file, if any, when starting
-the whole compilation process.
-
-Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look
-for name resolutions in the file ``file`` (it will look in ``file.glob``
-by default).
-
-Identifiers from the |Coq| standard library are linked to the Coq website
-`<http://coq.inria.fr/library/>`_. This behavior can be changed
-using command line options ``--no-externals`` and ``--coqlib``; see below.
-
-
-Hiding / Showing parts of the source.
-+++++++++++++++++++++++++++++++++++++
-
-Some parts of the source can be hidden using command line options ``-g``
-and ``-l`` (see below), or using such comments:
-
-::
-
-
-    (* begin hide *)
-     *some Coq material*
-    (* end hide *)
-
-
-Conversely, some parts of the source which would be hidden can be
-shown using such comments:
-
-::
-
-
-    (* begin show *)
-     *some Coq material*
-    (* end show *)
-
-
-The latter cannot be used around some inner parts of a proof, but can
-be used around a whole proof.
-
-
-Usage
-~~~~~
-
-coqdoc is invoked on a shell command line as follows:
-``coqdoc <options and files>``.
-Any command line argument which is not an option is considered to be a
-file (even if it starts with a ``-``). |Coq| files are identified by the
-suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``.
-
-
-:HTML output: This is the default output format. One HTML file is created for
-  each |Coq| file given on the command line, together with a file
-  ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a
-  style sheet named ``style.css``. Such a file is distributed with coqdoc.
-:|Latex| output: A single |Latex| file is created, on standard
-  output. It can be redirected to a file using the option ``-o``. The order of
-  files on the command line is kept in the final document. |Latex|
-  files given on the command line are copied ‘as is’ in the final
-  document . DVI and PostScript can be produced directly with the
-  options ``-dvi`` and ``-ps`` respectively.
-:TEXmacs output: To translate the input files to TEXmacs format,
-  to be used by the TEXmacs |Coq| interface.
-
-
-
-Command line options
-++++++++++++++++++++
-
-
-**Overall options**
-
-
-  :--HTML: Select a HTML output.
-  :--|Latex|: Select a |Latex| output.
-  :--dvi: Select a DVI output.
-  :--ps: Select a PostScript output.
-  :--texmacs: Select a TEXmacs output.
-  :--stdout: Write output to stdout.
-  :-o file, --output file: Redirect the output into the file ‘file’
-    (meaningless with ``-html``).
-  :-d dir, --directory dir: Output files into directory ‘dir’ instead of
-    the current directory (option ``-d`` does not change the filename specified
-    with the option ``-o``, if any).
-  :--body-only: Suppress the header and trailer of the final document.
-    Thus, you can insert the resulting document into a larger one.
-  :-p string, --preamble string: Insert some material in the |Latex|
-    preamble, right before ``\begin{document}`` (meaningless with ``-html``).
-  :--vernac-file file,--tex-file file: Considers the file ‘file’
-    respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file.
-  :--files-from file: Read filenames to be processed from the file ‘file’ as if
-    they were given on the command line. Useful for program sources split
-    up into several directories.
-  :-q, --quiet: Be quiet. Do not print anything except errors.
-  :-h, --help: Give a short summary of the options and exit.
-  :-v, --version: Print the version and exit.
-
-
-
-**Index options**
-
-  The default behavior is to build an index, for the HTML output only,
-  into ``index.html``.
-
-  :--no-index: Do not output the index.
-  :--multi-index: Generate one page for each category and each letter in
-    the index, together with a top page ``index.html``.
-  :--index string: Make the filename of the index string instead of
-    “index”. Useful since “index.html” is special.
-
-
-
-**Table of contents option**
-
-  :-toc, --table-of-contents: Insert a table of contents. For a |Latex|
-    output, it inserts a ``\tableofcontents`` at the beginning of the
-    document. For a HTML output, it builds a table of contents into
-    ``toc.html``.
-  :--toc-depth int: Only include headers up to depth ``int`` in the table of
-    contents.
-
-
-**Hyperlink options**
-
-  :--glob-from file: Make references using |Coq| globalizations from file
-    file. (Such globalizations are obtained with Coq option ``-dump-glob``).
-  :--no-externals: Do not insert links to the |Coq| standard library.
-  :--external url coqdir: Use given URL for linking references whose
-    name starts with prefix ``coqdir``.
-  :--coqlib url: Set base URL for the Coq standard library (default is
-    `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url
-    Coq``.
-  :-R dir coqdir: Recursively map physical directory dir to |Coq| logical
-    directory  ``coqdir`` (similarly to |Coq| option ``-R``).
-  :-Q dir coqdir: Map physical directory dir to |Coq| logical
-    directory  ``coqdir`` (similarly to |Coq| option ``-Q``).
-
-    .. note::
-
-       options ``-R`` and ``-Q`` only have
-       effect on the files *following* them on the command line, so you will
-       probably need to put this option first.
-
-
-**Title options**
-
-  :-s , --short: Do not insert titles for the files. The default
-     behavior is to insert a title like “Library Foo” for each file.
-  :--lib-name string: Print “string Foo” instead of “Library Foo” in
-     titles. For example “Chapter” and “Module” are reasonable choices.
-  :--no-lib-name: Print just “Foo” instead of “Library Foo” in titles.
-  :--lib-subtitles: Look for library subtitles. When enabled, the
-     beginning of each file is checked for a comment of the form:
-
-     ::
-
-        (** * ModuleName : text *)
-
-     where ``ModuleName`` must be the name of the file. If it is present, the
-     text is used as a subtitle for the module in appropriate places.
-  :-t string, --title string: Set the document title.
-
-
-**Contents options**
-
-  :-g, --gallina: Do not print proofs.
-  :-l, --light: Light mode. Suppress proofs (as with ``-g``) and the following commands:
-
-      + [Recursive] Tactic Definition
-      + Hint / Hints
-      + Require
-      + Transparent / Opaque
-      + Implicit Argument / Implicits
-      + Section / Variable / Hypothesis / End
-
-
-
-    The behavior of options ``-g`` and ``-l`` can be locally overridden using the
-    ``(* begin show *) … (* end show *)`` environment (see above).
-
-    There are a few options that control the parsing of comments:
-
-  :--parse-comments: Parse regular comments delimited by ``(*`` and ``*)`` as
-    well. They are typeset inline.
-  :--plain-comments: Do not interpret comments, simply copy them as
-    plain-text.
-  :--interpolate: Use the globalization information to typeset
-    identifiers appearing in |Coq| escapings inside comments.
-
-**Language options**
-
-
-  The default behavior is to assume ASCII 7 bit input files.
-
-  :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to
-    --inputenc latin1 --charset iso-8859-1.
-  :-utf8, --utf8: Set --inputenc utf8x for |Latex| output and--charset
-    utf-8 for HTML output. Also use Unicode replacements for a couple of
-    standard plain ASCII notations such as → for ``->`` and ∀ for ``forall``. |Latex|
-    UTF-8 support can be found
-    at `<http://www.ctan.org/pkg/unicode>`_. For the interpretation of Unicode
-    characters by |Latex|, extra packages which coqdoc does not provide
-    by default might be required, such as textgreek for some Greek letters
-    or ``stmaryrd`` for some mathematical symbols. If a Unicode character is
-    missing an interpretation in the utf8x input encoding, add
-    ``\DeclareUnicodeCharacter{code}{LATEX-interpretation}``. Packages
-    and declarations can be added with option ``-p``.
-  :--inputenc string: Give a |Latex| input encoding, as an option to |Latex|
-    package ``inputenc``.
-  :--charset string: Specify the HTML character set, to be inserted in
-    the HTML header.
-
-
-
-The coqdoc |Latex| style file
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-In case you choose to produce a document without the default |Latex|
-preamble (by using option ``--no-preamble``), then you must insert into
-your own preamble the command
-
-::
-
-  \usepackage{coqdoc}
-
-The package optionally takes the argument ``[color]`` to typeset
-identifiers with colors (this requires the ``xcolor`` package).
-
-Then you may alter the rendering of the document by redefining some
-macros:
-
-:coqdockw, coqdocid, …: The one-argument macros for typesetting
-  keywords and identifiers. Defaults are sans-serif for keywords and
-  italic for identifiers.For example, if you would like a slanted font
-  for keywords, you may insert
-
-  ::
-
-         \renewcommand{\coqdockw}[1]{\textsl{#1}}
-
-
-  anywhere between ``\usepackage{coqdoc}`` and ``\begin{document}``.
-
-
-:coqdocmodule:
-  One-argument macro for typesetting the title of a ``.v``
-  file. Default is
-
-  ::
-
-      \newcommand{\coqdocmodule}[1]{\section*{Module #1}}
-
-  and you may redefine it using ``\renewcommand``.
-
 Embedded Coq phrases inside |Latex| documents
 ---------------------------------------------