diff --git a/progs64/VSUpile/Makefile b/progs64/VSUpile/Makefile index 88d337354..308bcc705 100644 --- a/progs64/VSUpile/Makefile +++ b/progs64/VSUpile/Makefile @@ -39,7 +39,7 @@ VOFILES = $(patsubst %.v,%.vo,$(CVFILES) $(VFILES)) VST_DIRS= msl shared sepcomp veric zlist floyd -VSTFLAGS= -R $(VST_LOC)/compcert compcert $(foreach d, $(VST_DIRS), -Q $(VST_LOC)/$(d) VST.$(d)) -R . pile +VSTFLAGS= -R $(VST_LOC)/compcert compcert -Q $(VST_LOC)/ora/theories iris_ora $(foreach d, $(VST_DIRS), -Q $(VST_LOC)/$(d) VST.$(d)) -R . pile target: _CoqProject verif_main.vo simple_verif_main.vo fast/verif_fastmain.vo