helm/metadata/create/Makefile

   1 marcello_THEORIES_OK = \
   2  cic:/Coq/Arith/ \
   3  cic:/Coq/Bool/ \
   4  cic:/Coq/Init/ \
   5 \
   6  cic:/Coq/IntMap/Adalloc/ \
   7  cic:/Coq/IntMap/Addec/ \
   8  cic:/Coq/IntMap/Addr/ \
   9  cic:/Coq/IntMap/Adist/ \
  10  cic:/Coq/IntMap/Fset/ \
  11  cic:/Coq/IntMap/Lsort/ \
  12  cic:/Coq/IntMap/Map/ \
  13  cic:/Coq/IntMap/Mapaxioms/ \
  14  cic:/Coq/IntMap/Mapc/ \
  15  cic:/Coq/IntMap/Mapcanon/ \
  16  cic:/Coq/IntMap/Mapcard/ \
  17  cic:/Coq/IntMap/Mapfold/ \
  18  cic:/Coq/IntMap/Mapiter/ \
  19  cic:/Coq/IntMap/Maplists/ \
  20  cic:/Coq/IntMap/Mapsubset/ \
  21 \
  22  cic:/Coq/Lists/ \
  23  cic:/Coq/Logic/ \
  24 \
  25  cic:/Coq/Reals/R_Ifp/ \
  26  cic:/Coq/Reals/Raxioms/ \
  27  cic:/Coq/Reals/Rbase/ \
  28  cic:/Coq/Reals/Rbasic_fun/ \
  29  cic:/Coq/Reals/Rdefinitions/ \
  30  cic:/Coq/Reals/Rderiv/ \
  31  cic:/Coq/Reals/Rfunctions/ \
  32  cic:/Coq/Reals/Rlimit/ \
  33  cic:/Coq/Reals/Rseries/ \
  34  cic:/Coq/Reals/Rsyntax/ \
  35  cic:/Coq/Reals/Rtrigo_fun/ \
  36  cic:/Coq/Reals/TypeSyntax/ \
  37 \
  38  cic:/Coq/Relations/ \
  39  cic:/Coq/Sets/ \
  40  cic:/Coq/Wellfounded/ \
  41 \
  42  cic:/Coq/ZArith/Wf_Z/ \
  43  cic:/Coq/ZArith/ZArith_dec/ \
  44  cic:/Coq/ZArith/Zmisc/ \
  45  cic:/Coq/ZArith/Zsyntax/ \
  46  cic:/Coq/ZArith/auxiliary/ \
  47  cic:/Coq/ZArith/fast_integer/ \
  48  cic:/Coq/ZArith/zarith_aux/ \
  49 \
  50  cic:/Coq/correctness/ \
  51  cic:/Coq/field/ \
  52  cic:/Coq/fourier/ \
  53 \
  54  cic:/Coq/omega/Zcomplements/ \
  55  cic:/Coq/omega/Zlogarithm/ \
  56  cic:/Coq/omega/Zpower/ \
  57 \
  58  cic:/Coq/ring/ \
  59
  60 marcello:
  61         time ./mywget.pl $($@_THEORIES_OK)
  62
  63 rdf:
  64         ./split.pl output/*
  65         find rdf -type f -exec ./fix_rdf.pl {} \;
  66         (cd rdf ; ../mkindex.sh)
  67
  68 .PHONY: clean rdf clean-rdf
  69 clean:
  70         rm -f output/*
  71
  72 clean-rdf:
  73         rm -rf rdf/*