diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-01 12:30:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-01 12:30:52 +0000 |
| commit | 5a87d97bd8bce29d3c94bd40e4ab03c4c7c098a8 (patch) | |
| tree | 3ad8750efcbc0bea1c4fc2dcbb57251391bf8a93 /parsing/g_vernac.ml4 | |
| parent | bd358a1f07807970bebf73f14f0ec941e34d9737 (diff) | |
Ajout possibilité clause "where" dans co-points fixes
(+ uniformisation position notation dans les blocs inductifs et récursifs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 737c97bae..510fe529f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -191,9 +191,9 @@ GEXTEND Gram ; (* Inductives and records *) inductive_definition: - [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; + [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; ":="; lc = constructor_list; ntn = decl_notation -> - (id,ntn,indpar,c,lc) ] ] + ((id,indpar,c,lc),ntn) ] ] ; constructor_list: [ [ "|"; l = LIST1 constructor SEP "|" -> l @@ -212,7 +212,7 @@ GEXTEND Gram (* (co)-fixpoints *) rec_definition: [ [ id = ident; bl = LIST1 binder_let; - annot = rec_annotation; type_ = type_cstr; + annot = rec_annotation; ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> let names = List.map snd (names_of_local_assums bl) in let ni = @@ -227,12 +227,12 @@ GEXTEND Gram otherwise, we search the recursive index later *) if List.length names = 1 then Some 0 else None in - ((id, (ni, snd annot), bl, type_, def),ntn) ] ] + ((id,(ni,snd annot),bl,ty,def),ntn) ] ] ; corec_definition: - [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":="; - def = lconstr -> - (id,bl,c ,def) ] ] + [ [ id = ident; bl = LIST0 binder_let; ty = type_cstr; ":="; + def = lconstr; ntn = decl_notation -> + ((id,bl,ty,def),ntn) ] ] ; rec_annotation: [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) |