From 2fbdb0c45f0913b9fd8e95606c525fc5bfb3bc6d Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 28 Apr 2017 15:35:43 +0200
Subject: Issue #179: clightgen produces wrong abstract syntax for "switch"
 statements

---
 exportclight/ExportClight.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'exportclight')

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 003e97ee..8001dca7 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -124,6 +124,11 @@ let coqsingle p n =
 let coqN p n =
   fprintf p "%ld%%N" (N.to_int32 n)
 
+let coqZ p n =
+  if Z.ge n Z.zero
+  then fprintf p "%s" (Z.to_string n)
+  else fprintf p "(%s)" (Z.to_string n)
+
 (* Coq strings *)
 
 let coqstring p s =
@@ -364,10 +369,10 @@ let rec stmt p = function
 
 and lblstmts p = function
   | LSnil ->
-      ()
+      (fprintf p "LSnil")
   | LScons(lbl, s, ls) ->
-      fprintf p "@[<hv 2>(LScase %a@ %a@ %a)@]"
-              (print_option coqint) lbl stmt s lblstmts ls
+      fprintf p "@[<hv 2>(LScons %a@ %a@ %a)@]"
+              (print_option coqZ) lbl stmt s lblstmts ls
 
 let print_function p (id, f) =
   fprintf p "Definition f_%s := {|@ " (extern_atom id);
-- 
cgit