diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 14:11:31 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 14:11:31 +0100 |
| commit | cbc198ed8447e2089af65f790ceac6c620d361f5 (patch) | |
| tree | 43f66ba1f7448567e290dce961bdecd23b060d05 /cfrontend/PrintCsyntax.ml | |
| parent | 26908c322fd817007f3a8e7ef99108cc2d52b317 (diff) | |
| download | compcert-kvx-cbc198ed8447e2089af65f790ceac6c620d361f5.tar.gz compcert-kvx-cbc198ed8447e2089af65f790ceac6c620d361f5.zip | |
Removed shadowing problems.
The clashing identifiers are now referenced explicitly.
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index e3e259f7..6366906a 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -19,9 +19,9 @@ open Format open Camlcoq open Values open AST -open !Ctypes +open Ctypes open Cop -open !Csyntax +open Csyntax let name_unop = function | Onotbool -> "!" @@ -87,11 +87,11 @@ let rec name_cdecl id ty = match ty with | Tvoid -> "void" ^ name_optid id - | Tint(sz, sg, a) -> + | Ctypes.Tint(sz, sg, a) -> name_inttype sz sg ^ attributes a ^ name_optid id - | Tfloat(sz, a) -> + | Ctypes.Tfloat(sz, a) -> name_floattype sz ^ attributes a ^ name_optid id - | Tlong(sg, a) -> + | Ctypes.Tlong(sg, a) -> name_longtype sg ^ attributes a ^ name_optid id | Tpointer(t, a) -> let id' = @@ -182,7 +182,7 @@ let print_typed_value p v ty = fprintf p "%.15F" (camlfloat_of_coqfloat f) | Vsingle f, _ -> fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f) - | Vlong n, Tlong(Unsigned, _) -> + | Vlong n, Ctypes.Tlong(Unsigned, _) -> fprintf p "%LuLLU" (camlint64_of_coqint n) | Vlong n, _ -> fprintf p "%LdLL" (camlint64_of_coqint n) @@ -498,7 +498,7 @@ let print_globvar p id v = fprintf p "@[<hov 2>%s = " (name_cdecl name2 v.gvar_info); begin match v.gvar_info, v.gvar_init with - | (Tint _ | Tlong _ | Tfloat _ | Tpointer _ | Tfunction _), + | (Ctypes.Tint _ | Ctypes.Tlong _ | Ctypes.Tfloat _ | Tpointer _ | Tfunction _), [i1] -> print_init p i1 | _, il -> @@ -543,8 +543,8 @@ let print_program p prog = fprintf p "@[<v 0>"; List.iter (declare_composite p) prog.prog_types; List.iter (define_composite p) prog.prog_types; - List.iter (print_globdecl p) prog.prog_defs; - List.iter (print_globdef p) prog.prog_defs; + List.iter (print_globdecl p) prog.Ctypes.prog_defs; + List.iter (print_globdef p) prog.Ctypes.prog_defs; fprintf p "@]@." let destination : string option ref = ref None |