Skip to content

Commit

Permalink
readme, changes: Document the mquote directive
Browse files Browse the repository at this point in the history
  • Loading branch information
cpitclaudel committed Aug 26, 2021
1 parent 5134f66 commit e0c9eda
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 2 deletions.
4 changes: 3 additions & 1 deletion CHANGES.rst
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@
Unreleased
==========

- Alectryon now accepts a ``--pygments-style`` flag to chose which Pygments code-highlighting style to use. It also honors the Sphinx configuration option ``pygments_style``. [GH-58] [63539edd]
- A new ``mquote`` directive complements the ``mquote`` role by allowing authors to quote parts of a proof as a block (the ``mquote`` role generates inline text). [b38de96]

- Alectryon now accepts a ``--pygments-style`` flag to chose which Pygments code-highlighting style to use. It also honors the Sphinx configuration option ``pygments_style``. [GH-58] [63539ed]

- Alectryon now exists with an informative error code (``10`` + the level of the most severe Docutils error). [GH-57] [dffde22c]

Expand Down
6 changes: 5 additions & 1 deletion README.rst
Original file line number Diff line number Diff line change
Expand Up @@ -399,10 +399,14 @@ More details and examples are given in `<recipes/references.rst>`__.
Quoted references to goal fragments
***********************************

The `:mquote:` role is similar to `:mref:`, but it inserts a copy of the target instead of a link to it. Targets may only be hypotheses, goal conclusions, or goal or hypothesis names.
The ``:mquote:`` role is similar to ``:mref:``, but it inserts a copy of the target instead of a link to it. Targets may only be hypotheses, goal conclusions, or goal or hypothesis names.

For example, using :literal:`:mquote:\`.s(Induction).h#IHm.type\`` in the example above would print the type of ``IHm``, ``∀ n: ℕ, m + n = n + m`` whereas :literal:`:mref:\`.s(Induction).g#1.h(m + n = n + m).name\`` would produce only the name of the corresponding hypothesis, ``IHm``.

A ``.. mquote:`` directive is also available. It places the quoted elements in a block and preserves indentation and newlines, unlike the ``:mquote:`` role (whose output appears inline).

More details and examples are given in `<recipes/references.rst>`__.

Links to Coq identifiers
************************

Expand Down

0 comments on commit e0c9eda

Please sign in to comment.