From 1ab0d822649224201ce3c66e485f7fef5feb2196 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 31 Aug 2003 20:00:16 +0000
Subject: Syntaxe des constructeurs et des hypotheses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4286 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/syntax-v8.tex | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 76aace7947..6f59f53f2d 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -740,26 +740,26 @@ $$
        ~\OPT{\TERMbar}~\OPT{\NT{constructor-list}}
 \SEPDEF
 \DEFNT{constructor-list}
-       \NT{sbinder-coe}~\TERMbar~\NT{constructor-list}
-\nlsep \NT{sbinder-coe}
+       \NT{constructor}~\TERMbar~\NT{constructor-list}
+\nlsep \NT{constructor}
 \SEPDEF
 \DEFNT{constructor}
        \NT{ident}~\STAR{\NT{binder-let}}\OPTGR{\NT{coerce-kwd}~\NT{constr}}
 \SEPDEF
-\DEFNT{sbinder-coe}
-       \PLUS{\NT{ident}}~\OPTGR{\NT{coerce-kwd}~\NT{constr}}
-\SEPDEF
 \DEFNT{field-list}
        \NT{field}~\KWD{;}~\NT{field-list}
 \nlsep \NT{field}
+\SEPDEF
 \DEFNT{field}
        \NT{ident}~\OPTGR{\NT{coerce-kwd}~\NT{constr}}
 \nlsep \NT{ident}~\NT{type-cstr-coe}~\KWD{:=}~\NT{constr}
 \SEPDEF
-\SEPDEF
 \DEFNT{assum-list}
-       \NT{sbinder-coe}~\KWD{;}~\NT{assum-list}
-\nlsep \NT{sbinder-coe}
+       \PLUS{\GR{\KWD{(}~\NT{simple-assum-coe}~\KWD{)}}}
+\nlsep \NT{simple-assum-coe}
+\SEPDEF
+\DEFNT{simple-assum-coe}
+       \PLUS{\NT{ident}}~\NT{coerce-kwd}~\NT{constr}
 \SEPDEF
 \DEFNT{coerce-kwd} \TERM{:$>$} ~\mid~ \KWD{:}
 \SEPDEF
-- 
cgit v1.2.3