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

1 files changed, 9 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 5a0a6238d..dc2f65a15 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.