From 414ee07d82b093cec353fd67642818b75d0e23c5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 6 Jul 2007 13:53:32 +0000
Subject: Documentation related to commit 9948: intropattern {A,B,C} for
 (A,(B,C))

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9949 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 5a0a6238d6..dc2f65a152 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1484,6 +1484,15 @@ is a synonym for the pattern {\tt [$p_1$ {\ldots} $p_n$]}, i.e. it
 corresponds to the decomposition of an hypothesis typed by an
 inductive type with a single constructor.
 
+\Rem An additional abbreviation is allowed for sequences of rightmost
+binary conjonctions: pattern 
+{\tt \{} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt \}} 
+is a synonym for pattern 
+{\tt (} $p_1$ {\tt , (} $p_2$ {\tt ,} {\ldots} {\tt (}$p_{n-1}${\tt ,}$p_n${\tt )} {\ldots}  {\tt ))}.
+In particular it can be used to introduce existential hypothesis
+and/or n-ary conjonctions. 
+
+
 \begin{coq_example}
 Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
 intros A B C [a| [_ c]] f.
-- 
cgit v1.2.3