diff options
Diffstat (limited to 'backend/PrintAsmaux.ml')
-rw-r--r-- | backend/PrintAsmaux.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 13daa644..ed0fe524 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -51,6 +51,9 @@ module type TARGET = val new_label: unit -> int val label: out_channel -> int -> unit val print_file_loc: out_channel -> file_loc -> unit + val get_location: P.t -> location_value option + val get_segment_location: P.t -> location_value option + val add_var_location: P.t -> unit module DwarfAbbrevs: DWARF_ABBREVS end @@ -140,12 +143,6 @@ let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) (* Printing annotations in asm syntax *) -(** All files used in the debug entries *) -module StringSet = Set.Make(String) -let all_files : StringSet.t ref = ref StringSet.empty -let add_file file = - all_files := StringSet.add file !all_files - let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t = Hashtbl.create 7 |