diff --git a/docs/alpha/michelson.rst b/docs/alpha/michelson.rst
index 9af5628fb0d227224a3a1adf875cd91b7f222164..0f9530a00dbabb8e5f23f84f32c29cf2fde23f81 100644
--- a/docs/alpha/michelson.rst
+++ b/docs/alpha/michelson.rst
@@ -623,178 +623,17 @@ A detailed description of the following instructions can be found in the `intera
Operations on pairs and right combs
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The type ``pair l r`` is the type of binary pairs composed of a left
-element of type ``l`` and a right element of type ``r``. A value of
-type ``pair l r`` is written ``Pair x y`` where ``x`` is a value of
-type ``l`` and ``y`` is a value of type ``r``.
-
-To build tuples of length greater than 2, right combs have specific
-optimized operations. For any ``n > 2``, the compact notations ``pair
-t{0} t{1} ... t{n-2} t{n-1}`` is provided for the type of right combs
-``pair t{0} (pair t{1} ... (pair t{n-2} t{n-1}) ...)``. Similarly, the
-compact notation ``Pair x{0} x{1} ... x{n-2} x{n-1}`` is provided for
-the right-comb value ``Pair x{0} (Pair x{1} ... (Pair x{n-2} x{n-1})
-...)``. Right-comb values can also be written using sequences; ``Pair
-x{0} x{1} ... x{n-2} x{n-1}`` can be written ``{x{0}; x{1}; ...; x{n-2}; x{n-1}}``.
-
-- ``PAIR``: Build a binary pair from the stack's top two elements.
-
-::
-
- :: 'a : 'b : 'S -> pair 'a 'b : 'S
-
- > PAIR / x : y : S => Pair x y : S
-
-- ``PAIR n``: Fold ``n`` values on the top of the stack in a right comb.
- ``PAIR 0`` and ``PAIR 1`` are rejected. ``PAIR 2`` is equivalent to ``PAIR``.
-
-::
-
- PAIR 2 :: 'a : 'b : 'S -> pair 'a 'b : 'S
- PAIR (k+1) :: 'x : 'S -> pair 'x 'y : 'T
- iff PAIR k :: 'S -> 'y : 'T
-
- Or equivalently, for n >= 2,
- PAIR n :: 'a{0} : ... : 'a{n-1} : 'A -> pair 'a{0} ... 'a{n-1} : 'A
-
- > PAIR 2 / x : y : S => Pair x y : S
- > PAIR (k+1) / x : S => Pair x y : T
- iff PAIR k / S => y : T
-
- Or equivalently, for n >= 2,
- > PAIR n / x{0} : ... : x{n-1} : S => Pair x{0} ... x{n-1} : S
-
-- ``UNPAIR``: Split a pair into its components.
-
-::
-
- :: pair 'a 'b : 'S -> 'a : 'b : 'S
-
- > UNPAIR / Pair a b : S => a : b : S
-
-
-- ``UNPAIR n``: Unfold ``n`` values from a right comb on the top of the stack. ``UNPAIR 0`` and ``UNPAIR 1`` are rejected. ``UNPAIR 2`` is equivalent to ``UNPAIR``.
-
-::
-
- UNPAIR 2 :: pair 'a 'b : 'A -> 'a : 'b : 'A
- UNPAIR (k+1) :: pair 'a 'b : 'A -> 'a : 'B
- iff UNPAIR k :: 'b : 'A -> 'B
-
- Or equivalently, for n >= 2,
- UNPAIR n :: pair 'a{0} ... 'a{n-1} : S -> 'a{0} : ... : 'a{n-1} : S
-
- > UNPAIR 2 / Pair x y : S => x : y : S
- > UNPAIR (k+1) / Pair x y : SA => x : SB
- iff UNPAIR k / y : SA => SB
-
- Or equivalently, for n >= 2,
- > UNPAIR n / Pair x{0} ... x{n-1} : S => x{0} : ... : x{n-1} : S
-
-- ``CAR``: Access the left part of a pair.
-
-::
-
- :: pair 'a _ : 'S -> 'a : 'S
-
- > CAR / Pair x _ : S => x : S
-
-- ``CDR``: Access the right part of a pair.
-
-::
-
- :: pair _ 'b : 'S -> 'b : 'S
-
- > CDR / Pair _ y : S => y : S
-
-- ``GET k``: Access an element or a sub comb in a right comb.
-
- The nodes of a right comb of size ``n`` are canonically numbered as follows:
-
-::
-
- 0
- / \
- 1 2
- / \
- 3 4
- / \
- 5 ...
- 2n-2
- / \
- 2n-1 2n
-
-
-Or in plain English:
-
- - The root is numbered with 0,
- - The left child of the node numbered by ``k`` is numbered by ``k+1``, and
- - The right child of the node numbered by ``k`` is numbered by ``k+2``.
-
-The ``GET k`` instruction accesses the node numbered by ``k``. In
-particular, for a comb of size ``n``, the ``n-1`` first elements are
-accessed by ``GET 1``, ``GET 3``, ..., and ``GET (2n-1)`` and the last
-element is accessed by ``GET (2n)``.
-
-::
-
- GET 0 :: 'a : 'S -> 'a : 'S
- GET 1 :: pair 'x _ : 'S -> 'x : 'S
- GET (k+2) :: pair _ 'y : 'S -> 'z : 'S
- iff GET k :: 'y : 'S -> 'z : 'S
-
- Or equivalently,
- GET 0 :: 'a : 'S -> 'a : 'S
- GET (2k) :: pair 'a{0} ... 'a{k-1} 'a{k} : 'S -> 'a{k} : 'S
- GET (2k+1) :: pair 'a{0} ... 'a{k} 'a{k+1} : 'S -> 'a{k} : 'S
-
- > GET 0 / x : S => x : S
- > GET 1 / Pair x _ : S => x : S
- > GET (k+2) / Pair _ y : S => GET k / y : S
-
- Or equivalently,
- > GET 0 / x : S => x : S
- > GET (2k) / Pair x{0} ... x{k-1} x{k} : 'S -> x{k} : 'S
- > GET (2k+1) / Pair x{0} ... x{k} x{k+1} : 'S -> x{k} : 'S
-
-
-- ``UPDATE k``: Update an element or a sub comb in a right comb. The topmost stack element is the new value to insert in the comb, the second stack element is the right comb to update. The meaning of ``k`` is the same as for the ``GET k`` instruction.
-
-::
-
- UPDATE 0 :: 'a : 'b : 'S -> 'a : 'S
- UPDATE 1 :: 'a2 : pair 'a1 'b : 'S -> pair 'a2 'b : 'S
- UPDATE (k+2) :: 'c : pair 'a 'b1 : 'S -> pair 'a 'b2 : 'S
- iff UPDATE k :: 'c : 'b1 : 'S -> 'b2 : 'S
-
- Or equivalently,
- UPDATE 0 :: 'a : 'b : 'S -> 'a : 'S
- UPDATE (2k) :: 'c : pair 'a{0} ... 'a{k-1} 'a{k} : 'S -> pair 'a{0} ... 'a{k-1} 'c : 'S
- UPDATE (2k+1) :: 'c : pair 'a{0} ... 'a{k} 'a{k+1} : 'S -> pair 'a{0} ... 'a{k-1} 'c 'a{k+1} : 'S
-
- > UPDATE 0 / x : _ : S => x : S
- > UPDATE 1 / x2 : Pair x1 y : S => Pair x2 y : S
- > UPDATE (k+2) / z : Pair x y1 : S => Pair x y2 : S
- iff UPDATE k / z : y1 : S => y2 : S
-
- Or equivalently,
- > UPDATE 0 / x : _ : S => x : S
- > UPDATE (2k) / z : Pair x{0} ... x{k-1} x{k} : 'S => Pair x{0} ... x{k-1} z : 'S
- > UPDATE (2k+1) / z : Pair x{0} ... x{k-1} x{k} x{k+1} : 'S => Pair x{0} ... x{k-1} z x{k+1} : 'S
-
-- ``COMPARE``: Lexicographic comparison.
-
-::
-
- :: pair 'a 'b : pair 'a 'b : 'S -> int : 'S
+A detailed description of the following instructions can be found in the `interactive Michelson reference manual `__.
- > COMPARE / (Pair sa sb) : (Pair ta tb) : S => -1 : S
- iff COMPARE / sa : ta : S => -1 : S
- > COMPARE / (Pair sa sb) : (Pair ta tb) : S => 1 : S
- iff COMPARE / sa : ta : S => 1 : S
- > COMPARE / (Pair sa sb) : (Pair ta tb) : S => r : S
- iff COMPARE / sa : ta : S => 0 : S
- COMPARE / sb : tb : S => r : S
+- ``PAIR``: Build a binary pair from the stack's top two elements (`documentation `__).
+- ``PAIR n``: Fold ``n`` values on the top of the stack in a right comb (`documentation `__).
+- ``UNPAIR``: Split a pair into its components (`documentation `__).
+- ``UNPAIR n``: Unfold ``n`` values from a right comb on the top of the stack (`documentation `__).
+- ``CAR``: Access the left part of a pair (`documentation `__).
+- ``CDR``: Access the right part of a pair (`documentation `__).
+- ``GET k``: Access an element or a sub comb in a right comb (`documentation `__).
+- ``UPDATE k``: Update an element or a sub comb in a right comb (`documentation `__).
+- ``COMPARE``: Lexicographic comparison (`documentation `__).
Operations on sets
~~~~~~~~~~~~~~~~~~