diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/11859-warn-inexact-float.rst | 6 | ||||
| -rw-r--r-- | doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst | 7 | ||||
| -rw-r--r-- | doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst | 3 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/11725-cleanup-reals.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 464 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/coqdoc.rst | 463 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/index.rst | 1 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 16 | ||||
| -rw-r--r-- | doc/tools/docgram/README.md | 3 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 4 | ||||
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 33 | ||||
| -rw-r--r-- | doc/tools/docgram/dune | 63 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 4 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 4 |
17 files changed, 580 insertions, 535 deletions
diff --git a/doc/changelog/03-notations/11859-warn-inexact-float.rst b/doc/changelog/03-notations/11859-warn-inexact-float.rst new file mode 100644 index 0000000000..224ffdbe9b --- /dev/null +++ b/doc/changelog/03-notations/11859-warn-inexact-float.rst @@ -0,0 +1,6 @@ +- **Added:** + In primitive floats, print a warning when parsing a decimal value + that is not exactly a binary64 floating-point number. + For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't. + (`#11859 <https://github.com/coq/coq/pull/11859>`_, + by Pierre Roux). diff --git a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst new file mode 100644 index 0000000000..d510416990 --- /dev/null +++ b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst @@ -0,0 +1,7 @@ +- **Changed:** The :g:`auto with zarith` tactic and variations (including :tacn:`intuition`) + may now call the :tacn:`lia` tactic instead of :tacn:`omega` + (when the `Omega` module is loaded); + more goals may be automatically solved, + fewer section variables will be captured spuriously + (`#11018 <https://github.com/coq/coq/pull/11018>`_, + by Vincent Laporte). diff --git a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst new file mode 100644 index 0000000000..e409c638bb --- /dev/null +++ b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst @@ -0,0 +1,3 @@ +- **Removed:** Removed SearchAbout command that was deprecated in 8.5. + Use :cmd:`Search` instead. + (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle). diff --git a/doc/changelog/10-standard-library/11725-cleanup-reals.rst b/doc/changelog/10-standard-library/11725-cleanup-reals.rst new file mode 100644 index 0000000000..02ee7e6c70 --- /dev/null +++ b/doc/changelog/10-standard-library/11725-cleanup-reals.rst @@ -0,0 +1,6 @@ +- **Changed:** + Use implicit arguments for ``ConstructiveReals``. Move ``ConstructiveReals`` + into new directory ``Abstract``. Remove imports of implementations inside + those ``Abstract`` files. Move implementation by means of Cauchy sequences in new directory ``Cauchy``. + (`#11725 <https://github.com/coq/coq/pull/11725>`_, + by Vincent Semeria). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5ca0d8b81f..7401aff48c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -383,6 +383,10 @@ Changes in 8.11+beta1 <https://github.com/coq/coq/issues/3890>`_ and `#4638 <https://github.com/coq/coq/issues/4638>`_ by Maxime Dénès, review by Gaëtan Gilbert). +- **Changed:** + :cmd:`Fail` does not catch critical errors (including "stack overflow") + anymore (`#10173 <https://github.com/coq/coq/pull/10173>`_, + by Gaëtan Gilbert). - **Removed:** Undocumented :n:`Instance : !@type` syntax (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 39f2ccec29..acdd4408ed 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1062,6 +1062,11 @@ Floating-point constants are parsed and pretty-printed as (17-digit) decimal constants. This ensures that the composition :math:`\text{parse} \circ \text{print}` amounts to the identity. +.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing] + + Not all decimal constants are floating-point values. This warning + is generated when parsing such a constant (for instance ``0.1``). + .. example:: .. coqtop:: all 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 --------------------------------------------- diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c33d62532e..b22c5286fe 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -321,18 +321,6 @@ Requests to the environment Search (?x * _ + ?x * _)%Z outside OmegaLemmas. - .. cmdv:: SearchAbout - :name: SearchAbout - - .. deprecated:: 8.5 - - Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current - :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with - command :cmd:`SearchAbout`. For compatibility, the deprecated name - :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For - compatibility, the list of objects to search when using :cmd:`SearchAbout` - may also be enclosed by optional ``[ ]`` delimiters. - .. cmd:: SearchHead @term @@ -929,16 +917,17 @@ Quitting and debugging .. cmd:: Fail @command - For debugging scripts, sometimes it is desirable to know - whether a command or a tactic fails. If the given :n:`@command` - fails, the ``Fail`` statement succeeds, without changing the proof - state, and in interactive mode, the system - prints a message confirming the failure. - If the given :n:`@command` succeeds, the statement is an error, and - it prints a message indicating that the failure did not occur. + For debugging scripts, sometimes it is desirable to know whether a + command or a tactic fails. If the given :n:`@command` fails, then + :n:`Fail @command` succeeds (excepts in the case of + critical errors, like a "stack overflow"), without changing the + proof state, and in interactive mode, the system prints a message + confirming the failure. .. exn:: The command has not failed! - :undocumented: + + If the given :n:`@command` succeeds, then :n:`Fail @command` + fails with this error message. .. _controlling-display: diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst new file mode 100644 index 0000000000..cada680895 --- /dev/null +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -0,0 +1,463 @@ +.. _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``. diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst index 4381c4d63d..dfe38dfce9 100644 --- a/doc/sphinx/using/tools/index.rst +++ b/doc/sphinx/using/tools/index.rst @@ -16,5 +16,6 @@ on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. ../../practical-tools/coq-commands ../../practical-tools/utilities + coqdoc ../../practical-tools/coqide ../../addendum/parallel-proof-processing diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 0f05237036..e64b4be454 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -528,13 +528,17 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Reals/Rdefinitions.v - theories/Reals/ConstructiveReals.v - theories/Reals/ConstructiveRealsMorphisms.v - theories/Reals/ConstructiveCauchyReals.v - theories/Reals/ConstructiveCauchyRealsMult.v + theories/Reals/Cauchy/ConstructiveCauchyReals.v + theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v + theories/Reals/Cauchy/ConstructiveCauchyAbs.v theories/Reals/ClassicalDedekindReals.v theories/Reals/Raxioms.v - theories/Reals/ConstructiveRealsLUB.v + theories/Reals/Abstract/ConstructiveReals.v + theories/Reals/Abstract/ConstructiveRealsMorphisms.v + theories/Reals/Abstract/ConstructiveLUB.v + theories/Reals/Abstract/ConstructiveAbs.v + theories/Reals/Abstract/ConstructiveLimits.v + theories/Reals/Abstract/ConstructiveSum.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v @@ -579,7 +583,7 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Rcomplete.v - theories/Reals/ConstructiveRcomplete.v + theories/Reals/Cauchy/ConstructiveRcomplete.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rpow_def.v diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 7ae98f4cd2..4cde3809f0 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -110,6 +110,9 @@ Other command line arguments: * `-no-warn` suppresses printing of some warning messages +* `-no-update` puts updates to `fullGrammar` and `orderedGrammar` into new files named + `*.new`, leaving the originals unmodified. For use in Dune. + * `-short` limits processing to updating/verifying only the `fullGrammar` file * `-verbose` prints more messages about the grammar diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 88a5217652..60b845c4be 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1125,10 +1125,6 @@ query_command: [ | WITH "SearchRewrite" constr_pattern in_or_out_modules | REPLACE "Search" searchabout_query searchabout_queries "." | WITH "Search" searchabout_query searchabout_queries -| REPLACE "SearchAbout" searchabout_query searchabout_queries "." -| WITH "SearchAbout" searchabout_query searchabout_queries -| REPLACE "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." -| WITH "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules ] vernac_toplevel: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 0450aee2ec..eea1d5081d 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -32,6 +32,7 @@ type args = { fullGrammar : bool; check_tacs : bool; check_cmds : bool; + no_update: bool; show_warn : bool; verbose : bool; verify : bool; @@ -43,6 +44,7 @@ let default_args = { fullGrammar = false; check_tacs = false; check_cmds = false; + no_update = false; show_warn = true; verbose = false; verify = false; @@ -1574,7 +1576,7 @@ let reorder_grammar eg reordered_rules file = g_reorder eg !og.map !og.order -let finish_with_file old_file verify = +let finish_with_file old_file args = let files_eq f1 f2 = let chunksize = 8192 in (try @@ -1605,18 +1607,18 @@ let finish_with_file old_file verify = with Sys_error _ -> false) in - let temp_file = (old_file ^ "_temp") in + let temp_file = (old_file ^ ".new") in if !exit_code <> 0 then Sys.remove temp_file - else if verify then begin + else if args.verify then begin if not (files_eq old_file temp_file) then error "%s is not current\n" old_file; Sys.remove temp_file - end else + end else if not args.no_update then Sys.rename temp_file old_file let open_temp_bin file = - open_out_bin (sprintf "%s_temp" file) + open_out_bin (sprintf "%s.new" file) let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+" @@ -1829,7 +1831,7 @@ let process_rst g file args seen tac_prods cmd_prods = with End_of_file -> (); close_in old_rst; close_out new_rst; - finish_with_file file args.verify + finish_with_file file args let report_omitted_prods entries seen label split = let maybe_warn first last n = @@ -1877,7 +1879,7 @@ let process_grammar args = "DOC_GRAMMAR"; print_in_order out g `MLG !g.order StringSet.empty; close_out out; - finish_with_file (dir "fullGrammar") args.verify; + finish_with_file (dir "fullGrammar") args; if args.verbose then print_special_tokens g; @@ -1896,7 +1898,7 @@ let process_grammar args = "DOC_GRAMMAR"; print_in_order out g `MLG !g.order StringSet.empty; close_out out; - finish_with_file (dir "editedGrammar") args.verify; + finish_with_file (dir "editedGrammar") args; report_bad_nts g "editedGrammar" end; @@ -1911,11 +1913,13 @@ let process_grammar args = reorder_grammar g ordered_grammar "orderedGrammar"; print_in_order out g `MLG !g.order StringSet.empty; close_out out; - finish_with_file (dir "orderedGrammar") args.verify; + finish_with_file (dir "orderedGrammar") args; check_singletons g (* print_dominated g*) end; + let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in + let args = { args with no_update = false } in (* always update rsts in place for now *) if !exit_code = 0 then begin let plist nt = let list = (List.map (fun t -> String.trim (prod_to_prodn t)) @@ -1923,17 +1927,20 @@ let process_grammar args = list, StringSet.of_list list in let tac_list, tac_prods = plist "simple_tactic" in let cmd_list, cmd_prods = plist "command" in - let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files; report_omitted_prods !g.order !seen.nts "Nonterminal" ""; let out = open_out (dir "updated_rsts") in close_out out; + end; + (* if args.check_tacs then report_omitted_prods tac_list !seen.tacs "Tactic" "\n "; if args.check_cmds then report_omitted_prods cmd_list !seen.cmds "Command" "\n "; *) + + if !exit_code = 0 then begin (* generate report on cmds or tacs *) let cmdReport outfile cmdStr cmd_nts cmds cmdvs = let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings cmds)) in @@ -1942,7 +1949,7 @@ let process_grammar args = StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map))) ) StringSet.empty cmd_nts in let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in - let out = open_out_bin (dir outfile) in + let out = open_temp_bin (dir outfile) in StringSet.iter (fun c -> let rsts = StringSet.mem c rstCmds in let gram = StringSet.mem c gramCmds in @@ -1956,6 +1963,7 @@ let process_grammar args = fprintf out "%s%s %s\n" pfx var c) allCmds; close_out out; + finish_with_file (dir outfile) args; Printf.printf "# %s in rsts, gram, total = %d %d %d\n" cmdStr (StringSet.cardinal gramCmds) (StringSet.cardinal rstCmds) (StringSet.cardinal allCmds); in @@ -1973,7 +1981,7 @@ let process_grammar args = let out = open_temp_bin (dir "prodnGrammar") in print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty; close_out out; - finish_with_file (dir "prodnGrammar") args.verify + finish_with_file (dir "prodnGrammar") args end end @@ -1985,6 +1993,7 @@ let parse_args () = | "-check-cmds" -> { args with check_cmds = true } | "-check-tacs" -> { args with check_tacs = true } | "-no-warn" -> show_warn := false; { args with show_warn = true } + | "-no-update" -> { args with no_update = true } | "-short" -> { args with fullGrammar = true } | "-verbose" -> { args with verbose = true } | "-verify" -> { args with verify = true } diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 3afa21f2cf..fba4856241 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -5,26 +5,47 @@ (env (_ (binaries doc_grammar.exe))) (rule - (targets fullGrammar) + (alias check-gram) (deps - ; Main grammar - (glob_files %{project_root}/parsing/*.mlg) - (glob_files %{project_root}/toplevel/*.mlg) - (glob_files %{project_root}/vernac/*.mlg) - ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) - (glob_files %{project_root}/plugins/btauto/*.mlg) - (glob_files %{project_root}/plugins/cc/*.mlg) - (glob_files %{project_root}/plugins/derive/*.mlg) - (glob_files %{project_root}/plugins/extraction/*.mlg) - (glob_files %{project_root}/plugins/firstorder/*.mlg) - (glob_files %{project_root}/plugins/funind/*.mlg) - (glob_files %{project_root}/plugins/ltac/*.mlg) - (glob_files %{project_root}/plugins/micromega/*.mlg) - (glob_files %{project_root}/plugins/nsatz/*.mlg) - (glob_files %{project_root}/plugins/omega/*.mlg) - (glob_files %{project_root}/plugins/rtauto/*.mlg) - (glob_files %{project_root}/plugins/setoid_ring/*.mlg) - (glob_files %{project_root}/plugins/syntax/*.mlg)) + (:input + ; Main grammar + (glob_files %{project_root}/parsing/*.mlg) + (glob_files %{project_root}/toplevel/*.mlg) + (glob_files %{project_root}/vernac/*.mlg) + ; All plugins except SSReflect and Ltac2 for now (mimicking what is done in Makefile.doc) + (glob_files %{project_root}/plugins/btauto/*.mlg) + (glob_files %{project_root}/plugins/cc/*.mlg) + (glob_files %{project_root}/plugins/derive/*.mlg) + (glob_files %{project_root}/plugins/extraction/*.mlg) + (glob_files %{project_root}/plugins/firstorder/*.mlg) + (glob_files %{project_root}/plugins/funind/*.mlg) + (glob_files %{project_root}/plugins/ltac/*.mlg) + (glob_files %{project_root}/plugins/micromega/*.mlg) + (glob_files %{project_root}/plugins/nsatz/*.mlg) + (glob_files %{project_root}/plugins/omega/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/setoid_ring/*.mlg) + (glob_files %{project_root}/plugins/syntax/*.mlg) + ; Sphinx files + (glob_files %{project_root}/doc/sphinx/language/*.rst) + (glob_files %{project_root}/doc/sphinx/proof-engine/*.rst) + (glob_files %{project_root}/doc/sphinx/user-extensions/*.rst) + (glob_files %{project_root}/doc/sphinx/practical-tools/*.rst) + (glob_files %{project_root}/doc/sphinx/addendum/*.rst) + (glob_files %{project_root}/doc/sphinx/language/core/*.rst) + (glob_files %{project_root}/doc/sphinx/language/extensions/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/writing-proofs/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/automatic-tactics/*.rst) + (glob_files %{project_root}/doc/sphinx/proofs/creating-tactics/*.rst) + (glob_files %{project_root}/doc/sphinx/using/libraries/*.rst) + (glob_files %{project_root}/doc/sphinx/using/tools/*.rst)) + common.edit_mlg + orderedGrammar) (action - (chdir %{project_root} (run doc_grammar -short -no-warn %{deps}))) - (mode promote)) + (progn + (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.old; done") + (chdir %{project_root} (run doc_grammar -check-cmds %{input})) + (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.new; done") + (bash "for f in fullGrammar orderedGrammar; do cp ${f}.old ${f}; done") + (diff? fullGrammar fullGrammar.new) + (diff? orderedGrammar orderedGrammar.new)))) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 241cf48cf1..272d17bb35 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1244,8 +1244,6 @@ query_command: [ | "SearchPattern" constr_pattern in_or_out_modules "." | "SearchRewrite" constr_pattern in_or_out_modules "." | "Search" searchabout_query searchabout_queries "." -| "SearchAbout" searchabout_query searchabout_queries "." -| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." ] printable: [ @@ -2454,8 +2452,6 @@ as_or_and_ipat: [ eqn_ipat: [ | "eqn" ":" naming_intropattern -| "_eqn" ":" naming_intropattern -| "_eqn" | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 38e7b781df..0c9d7a853b 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -918,8 +918,6 @@ command: [ | "SearchPattern" one_term OPT ne_in_or_out_modules | "SearchRewrite" one_term OPT ne_in_or_out_modules | "Search" searchabout_query OPT searchabout_queries -| "SearchAbout" searchabout_query OPT searchabout_queries -| "SearchAbout" "[" LIST1 searchabout_query "]" OPT ne_in_or_out_modules | "Time" command | "Redirect" string command | "Timeout" num command @@ -1441,8 +1439,6 @@ as_or_and_ipat: [ eqn_ipat: [ | "eqn" ":" naming_intropattern -| "_eqn" ":" naming_intropattern -| "_eqn" ] as_name: [ |