From 0e96c241550c4a8abf65f3bb63fcd7cab3380e92 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 7 Aug 2020 20:54:55 -0700
Subject: Document semantic restriction on patterns

---
 doc/sphinx/language/core/variants.rst | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index d00a2f4100..8e2bf32dd6 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -57,6 +57,11 @@ Private (matching) inductive types
 Definition by cases: match
 --------------------------
 
+Objects of inductive types can be destructured by a case-analysis
+construction called *pattern matching* expression. A pattern matching
+expression is used to analyze the structure of an inductive object and
+to apply specific treatments accordingly.
+
 .. insertprodn term_match pattern0
 
 .. prodn::
@@ -77,10 +82,12 @@ Definition by cases: match
    | @numeral
    | @string
 
-Objects of inductive types can be destructured by a case-analysis
-construction called *pattern matching* expression. A pattern matching
-expression is used to analyze the structure of an inductive object and
-to apply specific treatments accordingly.
+Note that the :n:`@pattern ::= @pattern10 : @term` production
+is not supported in :n:`match` patterns.  Trying to use it will give this error:
+
+.. exn:: Casts are not supported in this pattern.
+   :undocumented:
+
 
 This paragraph describes the basic form of pattern matching. See
 Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
-- 
cgit v1.2.3