From c6d9d4fb142ef42634be25b60c0995b541e86629 Mon Sep 17 00:00:00 2001
From: Daniel de Rauglaudre
Date: Mon, 15 Feb 2016 16:22:45 +0100
Subject: Adding ability to put any pattern in binders, prefixed by a quote.

Cf CHANGES for details.
---
 doc/refman/RefMan-gal.tex | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-gal.tex')

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index fcccd9cb4b..99eee44e03 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -273,6 +273,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter
 {\binder} & ::= &   {\name} & (\ref{Binders}) \\
  & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\  
  & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
+ & $|$ & {\tt '} {\pattern} &\\
 & & &\\
 {\name} & ::= & {\ident} &\\
  & $|$ & {\tt \_} &\\
@@ -410,7 +411,8 @@ bound variable cannot be synthesized by the system, it can be
 specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt
 )}. There is also a notation for a sequence of binding variables
 sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt
-:}\,{\type}\,{\tt )}.
+:}\,{\type}\,{\tt )}. A binder can also be any pattern prefixed by a quote,
+e.g. {\tt '(x,y)}.
 
 Some constructions allow the binding of a variable to value. This is
 called a ``let-binder''. The entry {\binder} of the grammar accepts
-- 
cgit v1.2.3

