diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 71 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 79 |
3 files changed, 99 insertions, 84 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ad1f0caa60..9498f37c7e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -25,7 +25,7 @@ In the interactive mode, also known as the |Coq| toplevel, the user can develop his theories and proofs step by step. The |Coq| toplevel is run by the command ``coqtop``. -They are two different binary images of |Coq|: the byte-code one and the +There are two different binary images of |Coq|: the byte-code one and the native-code one (if OCaml provides a native-code compiler for your platform, which is supposed in the following). By default, ``coqtop`` executes the native-code version; run ``coqtop.byte`` to get @@ -43,10 +43,11 @@ The ``coqc`` command takes a name *file* as argument. Then it looks for a vernacular file named *file*.v, and tries to compile it into a *file*.vo file (See :ref:`compiled-files`). -.. caution:: The name *file* should be a - regular |Coq| identifier, as defined in Section :ref:'TODO-1.1'. It should contain - only letters, digits or underscores (_). For instance, ``/bar/foo/toto.v`` is valid, but - ``/bar/foo/to-to.v`` is invalid. +.. caution:: + + The name *file* should be a regular |Coq| identifier as defined in Section :ref:`lexical-conventions`. + It should contain only letters, digits or underscores (_). For example ``/bar/foo/toto.v`` is valid, + but ``/bar/foo/to-to.v`` is not. Customization at launch time @@ -59,8 +60,8 @@ When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will be implicitly prepended to any document read by Coq, whether it is an interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` -is the configuration directory of the user (by default its home -directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If +is the configuration directory of the user (by default it's ``~/.config``) +and ``xxx`` is the version number (e.g. 8.8). If this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, and, if still not found, the file ``~/.coqrc``. If the latter is also @@ -89,8 +90,8 @@ not set, they look for the commands in the executable path. The ``$COQ_COLORS`` environment variable can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated -list of assignments of the form ``name=``:n:``{*; attr}`` where -``name`` is the name of the corresponding highlight tag and each ``attrᵢ`` is an +list of assignments of the form :n:`name={*; attr}` where +``name`` is the name of the corresponding highlight tag and each ``attr`` is an ANSI escape code. The list of highlight tags can be retrieved with the ``-list-tags`` command-line option of ``coqtop``. @@ -103,10 +104,14 @@ The following command-line options are recognized by the commands ``coqc`` and ``coqtop``, unless stated otherwise: :-I *directory*, -include *directory*: Add physical path *directory* - to the OCaml loadpath. See also: :ref:`names-of-libraries` and the - command Declare ML Module Section :ref:`compiled-files`. + to the OCaml loadpath. + + .. seealso:: + + :ref:`names-of-libraries` and the + command Declare ML Module Section :ref:`compiled-files`. :-Q *directory* dirpath: Add physical path *directory* to the list of - directories where |Coq| looks for a file and bind it to the the logical + directories where |Coq| looks for a file and bind it to the logical directory *dirpath*. The subdirectory structure of *directory* is recursively available from |Coq| using absolute names (extending the dirpath prefix) (see Section :ref:`qualified-names`).Note that only those @@ -114,14 +119,17 @@ and ``coqtop``, unless stated otherwise: an :n:`@ident` are taken into account. Conversely, the underlying file systems or operating systems may be more restrictive than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive - layout (within the limit of 255 bytes per file name), the default on + layout (within the limit of 255 bytes per filename), the default on NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to disallow two files differing only in the case in the same directory. - See also: Section :ref:`names-of-libraries`. + + .. seealso:: Section :ref:`names-of-libraries`. :-R *directory* dirpath: Do as -Q *directory* dirpath but make the subdirectory structure of *directory* recursively visible so that the recursive contents of physical *directory* is available from |Coq| using - short or partially qualified names. See also: Section :ref:`names-of-libraries`. + short or partially qualified names. + + .. seealso:: Section :ref:`names-of-libraries`. :-top dirpath: Set the toplevel module name to dirpath instead of Top. Not valid for `coqc` as the toplevel module name is inferred from the name of the output file. @@ -140,15 +148,15 @@ and ``coqtop``, unless stated otherwise: :-l *file*, -load-vernac-source *file*: Load and execute the |Coq| script from *file.v*. :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the - |Coq| script from *file.v*. Output its content on the standard input as + |Coq| script from *file.v*. Write its contents to the standard output as it is executed. :-load-vernac-object dirpath: Load |Coq| compiled library dirpath. This is equivalent to runningRequire dirpath. :-require dirpath: Load |Coq| compiled library dirpath and import it. This is equivalent to running Require Import dirpath. :-batch: Exit just after argument parsing. Available for `coqtop` only. -:-compile *file.v*: Compile file *file.v* into *file.vo*. This options - imply -batch (exit just after argument parsing). It is available only +:-compile *file.v*: Compile file *file.v* into *file.vo*. This option + implies -batch (exit just after argument parsing). It is available only for `coqtop`, as this behavior is the purpose of `coqc`. :-compile-verbose *file.v*: Same as -compile but also output the content of *file.v* as it is compiled. @@ -167,11 +175,16 @@ and ``coqtop``, unless stated otherwise: :-emacs, -ide-slave: Start a special toplevel to communicate with a specific IDE. :-impredicative-set: Change the logical theory of |Coq| by declaring the - sort Set impredicative. Warning: This is known to be inconsistent with some - standard axioms of classical mathematics such as the functional - axiom of choice or the principle of description. -:-type-in-type: Collapse the universe hierarchy of |Coq|. Warning: This makes the logic - inconsistent. + sort Set impredicative. + + .. warning:: + + This is known to be inconsistent with some + standard axioms of classical mathematics such as the functional + axiom of choice or the principle of description. +:-type-in-type: Collapse the universe hierarchy of |Coq|. + + .. warning:: This makes the logic inconsistent. :-mangle-names *ident*: Experimental: Do not depend on this option. Replace Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, etc. The command ``Set Mangle Names`` turns the behavior on in a document, @@ -207,7 +220,7 @@ The ``coqchk`` command takes a list of library paths as argument, described eith by their logical name or by their physical filename, hich must end in ``.vo``. The corresponding compiled libraries (``.vo`` files) are searched in the path, recursively processing the libraries they depend on. The content of all these -libraries is then type-checked. The effect of ``coqchk`` is only to return with +libraries is then type checked. The effect of ``coqchk`` is only to return with normal exit code in case of success, and with positive exit code if an error has been found. Error messages are not deemed to help the user understand what is wrong. In the current version, it does not modify the compiled libraries to mark @@ -237,7 +250,7 @@ relative paths in object files ``-Q`` and ``-R`` have exactly the same meaning. unless explicitly required. :-o: At exit, print a summary about the context. List the names of all assumptions and variables (constants without body). -:-silent: Do not write progress information in standard output. +:-silent: Do not write progress information to the standard output. Environment variable ``$COQLIB`` can be set to override the location of the standard library. @@ -247,15 +260,15 @@ the following: assuming that ``coqchk`` is called with argument ``M``, option ``-norec N``, and ``-admit A``. Let us write :math:`\overline{S}` for the set of reflexive transitive dependencies of set :math:`S`. Then: -+ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type-checked before being added ++ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type checked before being added to the context. + And :math:`M \cup N \backslash C` is the set of modules that are loaded and added to the - context without type-checking. Basic integrity checks (checksums) are + context without type checking. Basic integrity checks (checksums) are nonetheless performed. -As a rule of thumb, the -admit can be used to tell that some libraries +As a rule of thumb, -admit can be used to tell Coq that some libraries have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` && -``coqchk B -admit A`` without type-checking any definition twice. Of +``coqchk B -admit A`` without type checking any definition twice. Of course, the latter is slightly slower since it makes more disk access. It is also less secure since an attacker might have replaced the compiled library ``A`` after it has been read by the first command, but diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index f9903e6104..bc6a074a27 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -12,7 +12,7 @@ file, executing corresponding commands or undoing them respectively. |CoqIDE| is run by typing the command `coqide` on the command line. Without argument, the main screen is displayed with an “unnamed -buffer”, and with a file name as argument, another buffer displaying +buffer”, and with a filename as argument, another buffer displaying the contents of that file. Additionally, `coqide` accepts the same options as `coqtop`, given in :ref:`thecoqcommands`, the ones having obviously no meaning for |CoqIDE| being ignored. @@ -27,7 +27,7 @@ is shown in the figure :ref:`CoqIDE main screen <coqide_mainscreen>`. At the top is a menu bar, and a tool bar below it. The large window on the left is displaying the various *script buffers*. The upper right window is the *goal window*, where -goals to prove are displayed. The lower right window is the *message +goals to be proven are displayed. The lower right window is the *message window*, where various messages resulting from commands are displayed. At the bottom is the status bar. @@ -62,8 +62,8 @@ In the figure :ref:`CoqIDE main screen <coqide_mainscreen>`, the running buffer is `Fermat.v`, all commands until the ``Theorem`` have been already executed, and the user tried to go forward executing ``Induction n``. That command failed because no such -tactic exists (tactics are now in lowercase…), and the wrong word is -underlined. +tactic exists (names of standard tactics are written in lowercase), +and the failing command is underlined. Notice that the processed part of the running buffer is not editable. If you ever want to modify something you have to go backward using the up @@ -82,8 +82,8 @@ background in the error background color (pink by default). The same characterization of error-handling applies when running several commands using the "goto" button. -If you ever try to execute a command which happens to run during a -long time, and would like to abort it before its termination, you may +If you ever try to execute a command that runs for a long time +and would like to abort it before it terminates, you may use the interrupt button (the white cross on a red circle). There are other buttons on the |CoqIDE| toolbar: a button to save the running @@ -92,7 +92,7 @@ buffers (left and right arrows); an "information" button; and a "gears" button. The "information" button is described in Section :ref:`try-tactics-automatically`. -The "gears" button submits proof terms to the |Coq| kernel for type-checking. +The "gears" button submits proof terms to the |Coq| kernel for type checking. When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. The presence of unchecked proof terms is indicated by ``Qed`` statements that @@ -141,11 +141,10 @@ Vernacular commands, templates The Templates menu allows using shortcuts to insert vernacular commands. This is a nice way to proceed if you are not sure of the -spelling of the command you want. +syntax of the command you want. -Moreover, this menu offers some *templates* which will automatic -insert a complex command like ``Fixpoint`` with a convenient shape for its -arguments. +Moreover, from this menu you can automatically insert templates of complex +commands like ``Fixpoint`` that you can conveniently fill afterwards. Queries ------------ @@ -177,7 +176,7 @@ The `Compile` menu offers direct commands to: Customizations ------------------- -You may customize your environment using menu Edit/Preferences. A new +You may customize your environment using the menu Edit/Preferences. A new window will be displayed, with several customization sections presented as a notebook. @@ -189,7 +188,7 @@ automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a third party, |CoqIDE| may read it again for you. Note that in the case -you edited that same file, you will be prompt to choose to either +you edited that same file, you will be prompted to choose to either discard your changes or not. The File charset encoding choice is described below in :ref:`character-encoding-saved-files`. @@ -209,7 +208,7 @@ Notice that these settings are saved in the file `.coqiderc` of your home directory. A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It -is not recommanded to edit this file manually: to modify a given menu +is not recommended to edit this file manually: to modify a given menu shortcut, go to the corresponding menu item without releasing the mouse button, press the key you want for the new shortcut, and release the mouse button afterwards. If your system does not allow it, you may @@ -240,14 +239,14 @@ mathematical symbols ∀ and ∃, you may define: There exists a small set of such notations already defined, in the file `utf8.v` of Coq library, so you may enable them just by -``Require utf8`` inside |CoqIDE|, or equivalently, by starting |CoqIDE| with -``coqide -l utf8``. +``Require Import Unicode.Utf8`` inside |CoqIDE|, or equivalently, +by starting |CoqIDE| with ``coqide -l utf8``. However, there are some issues when using such Unicode symbols: you of course need to use a character font which supports them. In the Fonts section of the preferences, the Preview line displays some Unicode symbols, so you could figure out if the selected font is OK. Related -to this, one thing you may need to do is choose whether GTK+ should +to this, one thing you may need to do is choosing whether GTK+ should use antialiased fonts or not, by setting the environment variable `GDK_USE_XFT` to 1 or 0 respectively. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index bdaa2aa1a2..218a19c2e5 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -43,7 +43,7 @@ Building a |Coq| project with coq_makefile The majority of |Coq| projects are very similar: a collection of ``.v`` files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of metadata needed in order to build the project are the command line -options to ``coqc`` (e.g. ``-R``, ``-I``, see also: Section +options to ``coqc`` (e.g. ``-R``, ``-I``, see also: section :ref:`command-line-options`). Collecting the list of files and options is the job of the ``_CoqProject`` file. @@ -107,7 +107,7 @@ decide how to build them. In particular: The use of ``.mlpack`` files has to be preferred over ``.mllib`` files, since it results in a “packed” plugin: All auxiliary modules (as -``Baz`` and ``Bazaux``) are hidden inside the plugin’s “name space” +``Baz`` and ``Bazaux``) are hidden inside the plugin’s "namespace" (``Qux_plugin``). This reduces the chances of begin unable to load two distinct plugins because of a clash in their auxiliary module names. @@ -218,6 +218,7 @@ file timing data: On ``Mac OS``, this works best if you’ve installed ``gnu-time``. .. example:: + For example, the output of ``make TIMED=1`` may look like this: @@ -295,6 +296,7 @@ file timing data: files which take effectively no time to compile. .. example:: + For example, the output table from ``make print-pretty-timed-diff`` may look like this: @@ -318,6 +320,7 @@ line timing data: line-by-line timing information. .. example:: + For example, running ``make all TIMING=1`` may result in a file like this: :: @@ -345,6 +348,7 @@ line timing data: This target requires python to build the table. .. example:: + For example, running ``print-pretty-single-time-diff`` might give a table like this: :: @@ -434,7 +438,7 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use For users of coq_makefile with version < 8.7 - + Support for “sub-directory” is deprecated. To perform actions before + + Support for "subdirectory" is deprecated. To perform actions before or after the build (like invoking ``make`` on a subdirectory) one can hook in pre-all and post-all extension points. + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target @@ -442,10 +446,10 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use -Modules dependencies +Module dependencies -------------------- -In order to compute modules dependencies (so to use ``make``), |Coq| comes +In order to compute module dependencies (so to use ``make``), |Coq| comes with an appropriate tool, ``coqdep``. ``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| @@ -460,7 +464,7 @@ command ``Declare ML Module``. Dependencies of |OCaml| modules are computed by looking at `open` commands and the dot notation *module.value*. However, this is done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| modules dependencies. +|OCaml| module dependencies. See the man page of ``coqdep`` for more details and options. @@ -478,9 +482,9 @@ 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 the |Coq| - sources, readable for a human and not only for the proof assistant; -#. to help the user navigating in his own (or third-party) sources. +#. 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. @@ -491,7 +495,7 @@ 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 pending ``*)``. The documentation format is inspired by Todd +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, @@ -507,7 +511,7 @@ 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. -Pre-formatted vernacular is enclosed by ``[[`` and ``]]``. The former must be +Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be followed by a newline and the latter must follow a newline. @@ -533,7 +537,7 @@ or It gives the |Latex| and HTML texts to be produced for the given |Coq| -token. One of the |Latex| or HTML text may be omitted, causing the +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 @@ -546,12 +550,12 @@ The printing for one token can be removed with Initially, the pretty-printing table contains the following mapping: -==== === ==== ===== === ==== ==== === -`->` → `<-` ← `*` × -`<=` ≤ `>=` ≥ `=>` ⇒ -`<>` ≠ `<->` ↔ `|-` ⊢ -`\/` ∨ `/\\` ∧ `~` ¬ -==== === ==== ===== === ==== ==== === +===== === ==== ===== === ==== ==== === +`->` → `<-` ← `*` × +`<=` ≤ `>=` ≥ `=>` ⇒ +`<>` ≠ `<->` ↔ `|-` ⊢ +`\\/` ∨ `/\\` ∧ `~` ¬ +===== === ==== ===== === ==== ==== === Any of these can be overwritten or suppressed using the printing commands. @@ -573,10 +577,9 @@ commands. Sections ++++++++ -Sections are introduced by 1 to 4 leading stars (i.e. at the beginning -of the line) followed by a space. One star is a section, two stars a -sub-section, etc. The section title is given on the remaining of the -line. +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:: @@ -624,7 +627,7 @@ More than 4 leading dashes produce a horizontal rule. Emphasis. +++++++++ -Text can be italicized by placing it in underscores. A non-identifier +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. @@ -679,16 +682,16 @@ 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 option ``--dump-glob +``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 into the file ``file`` (it will look in ``file.glob`` +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 web -site at `<http://coq.inria.fr/library/>`_. This behavior can be changed +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. @@ -731,12 +734,12 @@ 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. One HTML file is created for +: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 with option ``-o``. The order of + 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 @@ -762,15 +765,15 @@ Command line options :-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 - current directory (option ``-d`` does not change the filename specified - with option ``-o``, if any). + 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 file names to process in file ‘file’ as if + :--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. @@ -781,7 +784,7 @@ Command line options **Index options** - Default behavior is to build an index, for the HTML output only, + The default behavior is to build an index, for the HTML output only, into ``index.html``. :--no-index: Do not output the index. @@ -802,7 +805,7 @@ Command line options contents. -**Hyperlinks options** +**Hyperlink options** :--glob-from file: Make references using |Coq| globalizations from file file. (Such globalizations are obtained with Coq option ``-dump-glob``). @@ -858,9 +861,9 @@ Command line options 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 to drive the parsing of comments: + There are a few options that control the parsing of comments: - :--parse-comments: Parses regular comments delimited by ``(*`` and ``*)`` as + :--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. @@ -870,7 +873,7 @@ Command line options **Language options** - Default behavior is to assume ASCII 7 bits input files. + 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. @@ -935,7 +938,7 @@ macros: Embedded Coq phrases inside |Latex| documents --------------------------------------------- -When writing a documentation about a proof development, one may want +When writing documentation about a proof development, one may want to insert |Coq| phrases inside a |Latex| document, possibly together with the corresponding answers of the system. We provide a mechanical way to process such |Coq| phrases embedded in |Latex| files: the ``coq-tex`` |