aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintAsmaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/PrintAsmaux.ml')
-rw-r--r--backend/PrintAsmaux.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 324e7e66..2daa2d56 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -143,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