diff options
Diffstat (limited to 'doc/sphinx/language/gallina-extensions.rst')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 53b993edd..96e33cc26 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -379,6 +379,7 @@ we have the following equivalence Notice that the printing uses the :g:`if` syntax because `sumbool` is declared as such (see :ref:`controlling-match-pp`). +.. _irrefutable-patterns: Irrefutable patterns: the destructuring let variants ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |