From d033047de9bdcd90e79cd8f5316cdd0dd54788df Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 31 Mar 2020 10:46:11 +0100 Subject: Fix Makefile build --- Makefile | 7 +++++-- _CoqProject | 1 + 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 63d6436..17cf636 100644 --- a/Makefile +++ b/Makefile @@ -3,13 +3,16 @@ COMPCERTRECDIRS := lib common x86_64 x86 backend cfrontend driver flocq exportcl COMPCERTCOQINCLUDES := $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) -COQINCLUDES := -R src/common coqup.common -R src/verilog coqup.verilog -R src/extraction coqup.extraction -R src/translation coqup.translation $(COMPCERTCOQINCLUDES) +COQINCLUDES := -R src/common coqup.common -R src/verilog coqup.verilog \ + -R src/extraction coqup.extraction -R src/translation coqup.translation \ + -R src coqup $(COMPCERTCOQINCLUDES) COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source COQMAKE := "$(COQBIN)coq_makefile" COQUPDIRS := translation common verilog -VS := $(foreach d, $(COQUPDIRS), src/$(d)/*.v) +VSSUBDIR := $(foreach d, $(COQUPDIRS), src/$(d)/*.v) +VS := src/Compiler.v $(VSSUBDIR) .PHONY: all install proof clean diff --git a/_CoqProject b/_CoqProject index a1a5144..7b2f864 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,7 @@ -R src/extraction coqup.extraction -R src/translation coqup.translation -R src/verilog coqup.verilog +-R src coqup -R lib/CompCert/MenhirLib compcert.MenhirLib -R lib/CompCert/backend compcert.backend -- cgit