diff options
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; |