From dffc9885e54f9c68af23ec79023dfe8516a4cc32 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 16 Sep 2021 14:54:22 +0200
Subject: Add support to clightgen for generating Csyntax AST as .v files

As proposed in #404.

This is presented as a new option `-clight` to the existing `clightgen` tool.

Revise clightgen testing to test the Csyntax output in addition to
the Clight output.
---
 export/ExportClight.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'export/ExportClight.ml')

diff --git a/export/ExportClight.ml b/export/ExportClight.ml
index 421db5ed..e3b00986 100644
--- a/export/ExportClight.ml
+++ b/export/ExportClight.ml
@@ -233,7 +233,7 @@ let print_program p prog sourcefile normalized =
   name_program prog;
   fprintf p "@[<v 0>";
   fprintf p "%s" prologue;
-  print_clightgen_info ~sourcefile ~normalized p;
+  print_gen_info ~sourcefile ~normalized p;
   define_idents p;
   List.iter (print_globdef p) prog.Ctypes.prog_defs;
   fprintf p "Definition composites : list composite_definition :=@ ";
-- 
cgit