diff options
| -rw-r--r-- | powerpc/TargetPrinter.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 3f12a829..3d183972 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -648,7 +648,7 @@ module Target (System : SYSTEM):TARGET = fprintf oc " rldicl %a, %a, %ld, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) | Prldicr(r1, r2, c1, c2) -> - fprintf oc " rldicr %a, %a, %ld, %ld\n" + fprintf oc " rldicr %a, %a, %ld, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) | Prlwinm(r1, r2, c1, c2) -> let (mb, me) = rolm_mask (camlint_of_coqint c2) in |