marcello_THEORIES_OK = \
 cic:/Coq/Arith/ \
 cic:/Coq/Bool/ \
 cic:/Coq/Init/ \
\
 cic:/Coq/IntMap/Adalloc/ \
 cic:/Coq/IntMap/Addec/ \
 cic:/Coq/IntMap/Addr/ \
 cic:/Coq/IntMap/Adist/ \
 cic:/Coq/IntMap/Fset/ \
 cic:/Coq/IntMap/Lsort/ \
 cic:/Coq/IntMap/Map/ \
 cic:/Coq/IntMap/Mapaxioms/ \
 cic:/Coq/IntMap/Mapc/ \
 cic:/Coq/IntMap/Mapcanon/ \
 cic:/Coq/IntMap/Mapcard/ \
 cic:/Coq/IntMap/Mapfold/ \
 cic:/Coq/IntMap/Mapiter/ \
 cic:/Coq/IntMap/Maplists/ \
 cic:/Coq/IntMap/Mapsubset/ \
\
 cic:/Coq/Lists/ \
 cic:/Coq/Logic/ \
\
 cic:/Coq/Reals/R_Ifp/ \
 cic:/Coq/Reals/Raxioms/ \
 cic:/Coq/Reals/Rbase/ \
 cic:/Coq/Reals/Rbasic_fun/ \
 cic:/Coq/Reals/Rdefinitions/ \
 cic:/Coq/Reals/Rderiv/ \
 cic:/Coq/Reals/Rfunctions/ \
 cic:/Coq/Reals/Rlimit/ \
 cic:/Coq/Reals/Rseries/ \
 cic:/Coq/Reals/Rsyntax/ \
 cic:/Coq/Reals/Rtrigo_fun/ \
 cic:/Coq/Reals/TypeSyntax/ \
\
 cic:/Coq/Relations/ \
 cic:/Coq/Sets/ \
 cic:/Coq/Wellfounded/ \
\
 cic:/Coq/ZArith/Wf_Z/ \
 cic:/Coq/ZArith/ZArith_dec/ \
 cic:/Coq/ZArith/Zmisc/ \
 cic:/Coq/ZArith/Zsyntax/ \
 cic:/Coq/ZArith/auxiliary/ \
 cic:/Coq/ZArith/fast_integer/ \
 cic:/Coq/ZArith/zarith_aux/ \
\
 cic:/Coq/correctness/ \
 cic:/Coq/field/ \
 cic:/Coq/fourier/ \
\
 cic:/Coq/omega/Zcomplements/ \
 cic:/Coq/omega/Zlogarithm/ \
 cic:/Coq/omega/Zpower/ \
\
 cic:/Coq/ring/ \

marcello:
	time ./mywget.pl $($@_THEORIES_OK)

rdf:
	./split.pl output/*
	find rdf -type f -exec ./fix_rdf.pl {} \;
	(cd rdf ; ../mkindex.sh)

.PHONY: clean rdf clean-rdf
clean:
	rm -f output/*

clean-rdf:
	rm -rf rdf/*