From 5b53cb7b539420e869cc243ee4e94f81b1ed0bf4 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 28 Sep 2020 16:49:50 +0100
Subject: Fix compilation

---
 Makefile                 | 11 ++++++-----
 _CoqProject              |  6 +++---
 driver/VericertDriver.ml |  4 ++--
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/Makefile b/Makefile
index e1a93f6..e036d6f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,19 +1,20 @@
 UNAME_S := $(shell uname -s)
 ifeq ($(UNAME_S),Linux)
-	ARCH := x86_32-linux
+	ARCH := x86_64-linux
 endif
 ifeq ($(UNAME_S),Darwin)
-	ARCH := x86_32-macosx
+	ARCH := x86_64-macosx
 endif
 
-COMPCERTRECDIRS := lib common x86_32 x86 backend cfrontend driver flocq exportclight \
-  MenhirLib cparser
+COMPCERTRECDIRS := lib common x86_64 x86 backend cfrontend driver exportclight cparser
 
 COQINCLUDES := -R src/common vericert.common \
                -R src/extraction vericert.extraction \
                -R src/hls vericert.hls \
                -R src vericert \
-               $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
+               $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) \
+               -R lib/CompCert/flocq Flocq \
+               -R lib/CompCert/MenhirLib MenhirLib
 
 COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
 COQMAKE := $(COQBIN)coq_makefile
diff --git a/_CoqProject b/_CoqProject
index 72a2e4b..d54c15c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,14 +3,14 @@
 -R src/hls vericert.hls
 -R src vericert
 
--R lib/CompCert/MenhirLib compcert.MenhirLib
 -R lib/CompCert/backend compcert.backend
 -R lib/CompCert/cfrontend compcert.cfrontend
 -R lib/CompCert/common compcert.common
 -R lib/CompCert/cparser compcert.cparser
 -R lib/CompCert/driver compcert.driver
 -R lib/CompCert/exportclight compcert.exportclight
--R lib/CompCert/flocq compcert.flocq
 -R lib/CompCert/lib compcert.lib
 -R lib/CompCert/x86 compcert.x86
--R lib/CompCert/x86_32 compcert.x86_32
+-R lib/CompCert/x86_64 compcert.x86_64
+-R lib/CompCert/flocq Flocq
+-R lib/CompCert/MenhirLib MenhirLib
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 2b8d45f..f500499 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -91,14 +91,14 @@ let compile_c_file sourcename ifile ofile =
     close_out oc
   end else begin
     let verilog =
-      match Vericert.Compiler0.transf_hls_temp csyntax with
+      match Vericert.Compiler0.transf_hls csyntax with
       | Vericert.Errors.OK v ->
         v
       | Vericert.Errors.Error msg ->
         let loc = file_loc sourcename in
         fatal_error loc "%a"  print_error msg in
     let oc = open_out ofile in
-    Vericert.PrintRTLBlock.print_program oc verilog;
+    Vericert.PrintVerilog.print_program !option_debug_hls oc verilog;
     close_out oc
   end
 
-- 
cgit