summaryrefslogtreecommitdiff
path: root/backend/PrintCminor.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/PrintCminor.ml')
-rw-r--r--backend/PrintCminor.ml11
1 files changed, 7 insertions, 4 deletions
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 51a45b2..19f4c83 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -272,12 +272,15 @@ let rec print_stmt p s =
print_stmt s
| Sexit n ->
fprintf p "exit %d;" (Nat.to_int n)
- | Sswitch(e, cases, dfl) ->
- fprintf p "@[<v 2>switch (%a) {" print_expr e;
+ | Sswitch(long, e, cases, dfl) ->
+ fprintf p "@[<v 2>switch%s (%a) {"
+ (if long then "l" else "") print_expr e;
List.iter
(fun (n, x) ->
- fprintf p "@ case %ld: exit %d;"
- (camlint_of_coqint n) (Nat.to_int x))
+ fprintf p "@ case %s%s: exit %d;"
+ (Z.to_string n)
+ (if long then "LL" else "")
+ (Nat.to_int x))
cases;
fprintf p "@ default: exit %d;\n" (Nat.to_int dfl);
fprintf p "@;<0 -2>}@]"