From 5a86c7bb8c274ea41716b9002189d2644eb1c8c6 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 14 Feb 2020 15:47:07 +0000
Subject: Update makefile and Coq dependencies with CompCert

---
 Makefile     | 9 ++++++++-
 _CoqProject  | 3 ++-
 lib/CompCert | 2 +-
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/Makefile b/Makefile
index 9ef58ed..eff7f35 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,9 @@
-COQINCLUDES=-R src/CoqUp CoqUp
+COMPCERTRECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \
+  MenhirLib cparser
+
+COMPCERTCOQINCLUDES=$(foreach d, $(RECDIRS), -R lib/CompCert/$(d) compcert.$(d))
+
+COQINCLUDES=-R src/CoqUp CoqUp $(COMPCERTCOQINCLUDES)
 
 COQEXEC=$(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
 COQMAKE="$(COQBIN)coq_makefile"
@@ -8,6 +13,8 @@ VS=$(wildcard src/CoqUp/*.v)
 .PHONY: all install coq clean
 
 all:
+	(cd lib/CompCert && ./configure x86_64-linux)
+	$(MAKE) -C lib/CompCert all
 	$(MAKE) coq
 	$(MAKE) compile
 
diff --git a/_CoqProject b/_CoqProject
index 3fdb59f..3d5dae3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1 +1,2 @@
--R src/CoqUp CoqUp
+-R src/CoqUp CoqUp -R lib/CompCert/lib compcert.lib -R lib/CompCert/common compcert.common -R lib/CompCert/x86 compcert.x86 -R lib/CompCert/backend compcert.backend -R lib/CompCert/cfrontend compcert.cfrontend -R lib/CompCert/driver compcert.driver -R lib/CompCert/flocq compcert.flocq -R lib/CompCert/exportclight compcert.exportclight -R lib/CompCert/cparser compcert.cparser -R lib/CompCert/MenhirLib compcert.MenhirLib
+-R lib/CompCert/x86_64 compcert.x86_64
diff --git a/lib/CompCert b/lib/CompCert
index 9b881b7..bc0e157 160000
--- a/lib/CompCert
+++ b/lib/CompCert
@@ -1 +1 @@
-Subproject commit 9b881b7928ab7d21e9981133bef5b26e33b6cd9d
+Subproject commit bc0e1573c189e876ebaf377d11f2f8a00eb8dcf0
-- 
cgit