aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/PrintOp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/PrintOp.ml')
-rw-r--r--riscV/PrintOp.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 8ba72fb2..aa609e15 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -97,10 +97,10 @@ let print_condition reg pp = function
let print_operation reg pp = function
| Omove, [r1] -> reg pp r1
- | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n)
- | Olongconst n, [] -> fprintf pp "%LdL" (camlint64_of_coqint n)
- | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n)
- | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n)
+ | Ointconst n, [] -> fprintf pp "Ointconst(%ld)" (camlint_of_coqint n)
+ | Olongconst n, [] -> fprintf pp "Olongconst(%LdL)" (camlint64_of_coqint n)
+ | Ofloatconst n, [] -> fprintf pp "Ofloatconst(%F)" (camlfloat_of_coqfloat n)
+ | Osingleconst n, [] -> fprintf pp "Osingleconst(%Ff)" (camlfloat_of_coqfloat32 n)
| Oaddrsymbol(id, ofs), [] ->
fprintf pp "\"%s\" + %Ld" (extern_atom id) (camlint64_of_ptrofs ofs)
| Oaddrstack ofs, [] ->