readme: Document :mref:

CHANGES.rst

@@ -5,7 +5,7 @@
 Unreleased
 ==========
 
-- A new ``:href:`` role lets authors refer to specific to sentences, hypotheses, and goals within a fragment of Coq code. [8a02bce]
+- A new ``:mref:`` role lets authors refer to specific to sentences, hypotheses, and goals within a fragment of Coq code. [8a02bce]
 
 - Alectryon's LaTeX preamble has been rewritten to improve line breaking between and within hypotheses. [3325d55]
 

README.rst

@@ -265,6 +265,48 @@ Extra roles and directives
 
 For convenience, alectryon includes a few extra roles and directives:
 
+- ``:mref:`` (“marker reference”) can be used to point the reader to a sentence, a goal, or a hypothesis.  The argument is a search pattern; Alectryon locates the corresponding object in the input sent to the prover or in the prover's output, inserts a marker at that point, and replaces the reference with a link to that marker.
+
+  In the example below, the markers ``[α]``, ``[β]``, and ``[γ]`` were generated by the following commands:
+
+  .. code-block:: coq
+
+     Goal ∀ m n, m + n = n + m. [α]
+       induction m; intros.
+       - (* Base case *)
+         【 n: ℕ ⊢ 0 + n = n + 0 [β] 】
+         apply plus_n_O.
+       - (* Induction *)
+         【 m, n: ℕ; IHm: ∀ n: ℕ, m + n = n + m [γ]
+            ⊢ S m + n = n + S m 】
+
+  - ``[α]``
+
+    :literal:`:mref:\`Goal ∀\``
+       Plain-text search for a sentence.
+
+  - ``[β]``
+
+    :literal:`:mref:\`.s(Base case).ccl\``
+       Search for a ``.s``\ entence, then mark the conclusion of the first goal.
+
+  - ``[γ]``
+
+    :literal:`:mref:\`.s(Induction).h#IHm\``
+       Search for a ``.s``\ entence, then mark the ``.h``\ ypothesis ``IHm`` by name in the first goal.
+
+    :literal:`:mref:\`.s(Induction).g#1.h(m + n = n + m)\``
+       Search for a ``.s``\ entence, select the first ``.g``\ oal by ``#`` number, mark the ``.h``\ ypothesis ``IHm`` by searching for its contents.
+
+  Markers can be customized by setting the ``:counter-style:`` option on a custom role derived from ``:mref:``; for example, to use Devanagari numerals:
+
+  .. code-block::
+
+     .. role:: dref(mref)
+        :counter-style: ० १ २ ३ ४ ५ ६ ७ ८ ९
+
+  More details and examples are given in `<recipes/references.rst>`__.
+
 - ``:coqid:`` can be used to link to the documentation or definition of a Coq identifier in an external file.  Some examples:
 
   - :literal:`:coqid:\`Coq.Init.Nat.even\`` → `Coq.Init.Nat.even <https://coq.inria.fr/library/Coq.Init.Nat.html#even>`__