diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-10 13:35:48 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-10 13:35:48 +0100 |
| commit | 5b05d3668571bd9b748b781b0cc29ae10f745f61 (patch) | |
| tree | aa235b80ff0666c34332be46664ae289d8afaa2c /debug/Debug.ml | |
| parent | 272087e1bc62bead1d1e1bea3d64e12d013eea37 (diff) | |
| download | compcert-kvx-5b05d3668571bd9b748b781b0cc29ae10f745f61.tar.gz compcert-kvx-5b05d3668571bd9b748b781b0cc29ae10f745f61.zip | |
Code cleanup.
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
Diffstat (limited to 'debug/Debug.ml')
| -rw-r--r-- | debug/Debug.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/debug/Debug.ml b/debug/Debug.ml index 775a0903..7403d7c2 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -12,9 +12,8 @@ open AST open BinNums -open C +open !C open Camlcoq -open Dwarfgen open DwarfTypes open Sections @@ -32,7 +31,7 @@ type implem = add_fun_addr: atom -> section_name -> (int * int) -> unit; generate_debug_info: (atom -> string) -> string -> debug_entries option; all_files_iter: (string -> unit) -> unit; - insert_local_declaration: storage -> ident -> typ -> location -> unit; + insert_local_declaration: storage -> ident -> C.typ -> location -> unit; atom_local_variable: ident -> atom -> unit; enter_scope: int -> int -> int -> unit; enter_function_scope: int -> int -> unit; |