Document Asymmetric Patterns.

1 files changed, 12 insertions, 0 deletions

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 7ad895f9d..376ef031d 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -280,6 +280,18 @@ Fail Check
      end).
 \end{coq_example}
 
+The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns}
+(off by default) removes parameters from constructors in patterns:
+\begin{coq_example}
+  Set Asymmetric Patterns.
+  Check (fun l:List nat =>
+    match l with
+    | nil => nil
+    | cons _ l' => l'
+    end)
+  Unset Asymmetric Patterns.
+\end{coq_example}
+
 \paragraph{Implicit arguments in patterns}
 By default, implicit arguments are omitted in patterns. So we write: