aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight/Clightgen.ml
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight/Clightgen.ml')
-rw-r--r--exportclight/Clightgen.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index 4209975a..f7279a5e 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -45,7 +45,7 @@ let compile_c_ast sourcename csyntax ofile =
| Errors.Error msg ->
fatal_error loc "%a" print_error msg in
(* Dump Clight in C syntax if requested *)
- PrintClight.print_if clight;
+ PrintClight.print_if_2 clight;
(* Print Clight in Coq syntax *)
let oc = open_out ofile in
ExportClight.print_program (Format.formatter_of_out_channel oc)