From 0bca8c15643e7b5b894b822db4f50bfbbd0858bb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 24 Nov 2017 22:48:05 +0100
Subject: Document Asymmetric Patterns.

---
 doc/refman/Cases.tex | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 7ad895f9d8..376ef031db 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:
 
-- 
cgit v1.2.3