aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-08-31 20:00:16 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-08-31 20:00:16 +0000
commit1ab0d822649224201ce3c66e485f7fef5feb2196 (patch)
tree378436b0ebbdb858d65bd22970e0f0b51075dff4 /doc
parent225037d53e3c7f797ba822612ffa06578f48a0bd (diff)
Syntaxe des constructeurs et des hypotheses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4286 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r--doc/syntax-v8.tex16
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 76aace794..6f59f53f2 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