diff options
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/ExportClight.ml | 11 |
1 files changed, 8 insertions, 3 deletions
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); |