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 | |
| 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')
| -rw-r--r-- | parsing/g_vernac.ml4 | 14 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 8 |
2 files changed, 12 insertions, 10 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) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b3a8abce5..5e13a1124 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -530,7 +530,7 @@ let rec pr_vernac = function fnl() ++ str (if List.length l = 1 then " " else " | ") ++ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in - let pr_oneind key (id,ntn,indpar,s,lc) = + let pr_oneind key ((id,indpar,s,lc),ntn) = hov 0 ( str key ++ spc() ++ pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ @@ -585,14 +585,16 @@ let rec pr_vernac = function prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs) | VernacCoFixpoint (corecs,b) -> - let pr_onecorec (id,bl,c,def) = + let pr_onecorec ((id,bl,c,def),ntn) = let (bl',def,c) = if Options.do_translate() then extract_def_binders def c else ([],def,c) in let bl = bl @ bl' in pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ spc() ++ pr_lconstr_expr c ++ - str" :=" ++ brk(1,1) ++ pr_lconstr def in + str" :=" ++ brk(1,1) ++ pr_lconstr def ++ + pr_decl_notation pr_constr ntn + in let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in hov 1 (str start ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) |