Commit 03d92cfa authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Fix dependedncy between vo files in example/arith

parent ee9d6fdc
......@@ -17,10 +17,23 @@ INCLUDE_DIRS= -I ../../lib/logic -I ../../lib/arith/definitions -I ../../lib/ari
FOCALIZEC_OPT += -no-coq-code %.vo
( echo "Require Coqine.";\
echo "Require $*.";\
echo "Dedukti Export All.") | $(COQTOP)
# We have to generate all dks coming from coq at the same time
# so that universe consistency can be checked globally
COQMODULES = CoqNaturals sieve
VOS = $(V_FILES:.v=.vo)
sieve.vo: CoqNaturals.vo
.PHONY: dks_from_coqine
dks_from_coqine: $(VOS)
../../ $(COQMODULES) | $(COQTOP) dks_from_coqine dks_from_coqine
sieve.dko: CoqNaturals.dko
$(OPENTHEORY) info $* &> /dev/null || $(OPENTHEORY) install $*
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment