diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 14:13:19 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 14:13:19 +0100 |
commit | 163f4a4e4467f64759dfa67bd555e6b893692561 (patch) | |
tree | 81731eb1f0e6bdc6c1fc321d0b865bb056eef5cc /Makefile | |
parent | c68661bd1eb5565e1272e039d7c2fa34086abf90 (diff) | |
download | compcert-kvx-vericert.tar.gz compcert-kvx-vericert.zip |
Compile under the name: kvxvericert
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -36,18 +36,18 @@ DIRS := lib lib/Impure common $(ARCHDIRS) scheduling backend cfrontend driver \ RECDIRS:=lib common $(ARCHDIRS) scheduling backend cfrontend driver flocq exportclight \ cparser -COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(subst /,.,$d)) +COQINCLUDES := $(foreach d, $(DIRS), -R $(d) kvx.$(subst /,.,$d)) ifeq ($(LIBRARY_FLOCQ),local) DIRS += flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 RECDIRS += flocq -COQINCLUDES += -R flocq Flocq +COQINCLUDES += -R flocq kvx.Flocq endif ifeq ($(LIBRARY_MENHIRLIB),local) DIRS += MenhirLib RECDIRS += MenhirLib -COQINCLUDES += -R MenhirLib MenhirLib +COQINCLUDES += -R MenhirLib kvx.MenhirLib endif # Notes on silenced Coq warnings: @@ -402,7 +402,7 @@ check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." check-proof: $(FILES) - $(COQCHK) compcert.driver.Complements + $(COQCHK) kvx.driver.Complements print-includes: @echo $(COQINCLUDES) |