diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/PrintAsm.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index e5b21f9c..16f22d60 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -336,8 +336,6 @@ let print_instruction oc labels = function | Psufd(r1, r2, r3) -> fprintf oc " sufd %a, %a, %a\n" freg r1 freg r2 freg r3; 1 (* Pseudo-instructions *) - | Pallocblock -> - fprintf oc " bl compcert_alloc\n"; 1 | Pallocframe(lo, hi, ofs) -> let lo = camlint_of_coqint lo and hi = camlint_of_coqint hi |