diff options
| author | herbelin | 2006-09-01 12:30:52 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-01 12:30:52 +0000 |
| commit | 5a87d97bd8bce29d3c94bd40e4ab03c4c7c098a8 (patch) | |
| tree | 3ad8750efcbc0bea1c4fc2dcbb57251391bf8a93 /parsing/ppvernac.ml | |
| 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/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b3a8abce55..5e13a11245 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) |