aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight/Clightgen.ml
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight/Clightgen.ml')
-rw-r--r--exportclight/Clightgen.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index 9cb0674e..1eb4fe03 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -53,7 +53,8 @@ let compile_c_ast sourcename csyntax ofile =
end;
(* Print Clight in Coq syntax *)
let oc = open_out ofile in
- ExportClight.print_program (Format.formatter_of_out_channel oc) clight;
+ ExportClight.print_program (Format.formatter_of_out_channel oc)
+ clight sourcename !option_normalize;
close_out oc
(* From C source to Clight *)