diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-31 20:00:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-31 20:00:16 +0000 |
| commit | 1ab0d822649224201ce3c66e485f7fef5feb2196 (patch) | |
| tree | 378436b0ebbdb858d65bd22970e0f0b51075dff4 /doc | |
| parent | 225037d53e3c7f797ba822612ffa06578f48a0bd (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.tex | 16 |
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 |