aboutsummaryrefslogtreecommitdiffstats
path: root/x86
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-11-10 11:05:02 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-11-10 11:05:02 +0100
commita3ec645b5ae36c54988f95057f37693edbad02c5 (patch)
treec40bad8b98a9f9d802657b487d5916c2bc85a6ba /x86
parent2bf69a09c20c52685ce3c1933577b9aaa5e38e51 (diff)
downloadcompcert-a3ec645b5ae36c54988f95057f37693edbad02c5.tar.gz
compcert-a3ec645b5ae36c54988f95057f37693edbad02c5.zip
Remove no longer used function. Bug 22525
Diffstat (limited to 'x86')
-rw-r--r--x86/TargetPrinter.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 1525b49b..3171847c 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -867,8 +867,6 @@ module Target(System: SYSTEM):TARGET =
| [t;l;j] -> (t, l, j)
| _ -> (Section_text, Section_literal, Section_jumptable)
- let reset_constants = reset_constants
-
let print_fun_info = print_fun_info
let print_var_info = print_var_info