diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-06 16:53:12 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-06 16:53:12 +0100 |
| commit | 8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed (patch) | |
| tree | 43e89a45ed321081cbcaaac06165a7e62b84a34b /cparser/Cprint.ml | |
| parent | 9d4bb7ec914566b3920cca3c6823515448fb65c1 (diff) | |
| parent | 4afaf8c23274752c8a6067bd785e114578068702 (diff) | |
| download | compcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.tar.gz compcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.zip | |
Merge branch 'elaboration-of-attributes'
Diffstat (limited to 'cparser/Cprint.ml')
| -rw-r--r-- | cparser/Cprint.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 2a110104..0a927873 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -142,13 +142,14 @@ let rec dcl ?(pp_indication=true) pp ty n = dcl pp t n' | TArray(t, sz, a) -> let n' pp = + n pp; begin match a with - | [] -> n pp - | _ -> fprintf pp " (%a%t)" attributes a n + | [] -> fprintf pp "[" + | _ -> fprintf pp "[%a " attributes a end; begin match sz with - | None -> fprintf pp "[]" - | Some i -> fprintf pp "[%Ld]" i + | None -> fprintf pp "]" + | Some i -> fprintf pp "%Ld]" i end in dcl pp t n' | TFun(tres, args, vararg, a) -> @@ -156,10 +157,8 @@ let rec dcl ?(pp_indication=true) pp ty n = dcl pp ty (fun pp -> fprintf pp " %a" ident id) in let n' pp = - begin match a with - | [] -> n pp - | _ -> fprintf pp " (%a%t)" attributes a n - end; + attributes pp a; + n pp; fprintf pp "("; if pp_indication then fprintf pp "@[<hov 0>"; begin match args with |