helm/coq-contribs/SUBSETS/Makefile

   1 ##############################################################################
   2 ##                 The Calculus of Inductive Constructions                  ##
   3 ##                                                                          ##
   4 ##                                Projet Coq                                ##
   5 ##                                                                          ##
   6 ##                     INRIA                        ENS-CNRS                ##
   7 ##              Rocquencourt                        Lyon                    ##
   8 ##                                                                          ##
   9 ##                                  Coq V7                                  ##
  10 ##                                                                          ##
  11 ##                                                                          ##
  12 ##############################################################################
  13
  14 # WARNING
  15 #
  16 # This Makefile has been automagically generated by coq_makefile
  17 # Edit at your own risks !
  18 #
  19 # END OF WARNING
  20
  21 #
  22 # This Makefile was generated by the command line :
  23 # coq_makefile -f Make -o Makefile
  24 #
  25
  26 ##########################
  27 #                        #
  28 # Variables definitions. #
  29 #                        #
  30 ##########################
  31
  32 CAMLP4LIB=`camlp4 -where`
  33 COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
  34   -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
  35   -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
  36   -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
  37 ZFLAGS=$(OCAMLLIBS) $(COQSRC)
  38 OPT=
  39 COQFLAGS=-q $(OPT) $(COQLIBS)
  40 COQC=$(COQBIN)coqc
  41 GALLINA=gallina
  42 COQWEB=coqweb
  43 CAMLC=ocamlc -c
  44 CAMLOPTC=ocamlopt -c
  45 CAMLLINK=ocamlc
  46 CAMLOPTLINK=ocamlopt
  47 COQDEP=$(COQBIN)coqdep -c
  48 COQVO2XML=coq_vo2xml
  49
  50 #########################
  51 #                       #
  52 # Libraries definition. #
  53 #                       #
  54 #########################
  55
  56 OCAMLLIBS=-I .
  57 COQLIBS=-I .
  58
  59 ###################################
  60 #                                 #
  61 # Definition of the "all" target. #
  62 #                                 #
  63 ###################################
  64
  65 VFILES=st_base.v\
  66   st_logic.v\
  67   st_nat.v\
  68   st_arith.v\
  69   Standard.v\
  70   xt_fin.v\
  71   tbs_base.v\
  72   tbs_rel.v\
  73   tbs_op.v\
  74   tbs_rop.v\
  75   tbs_fun.v\
  76   tbs_fin.v\
  77   Toolbox.v
  78 VOFILES=$(VFILES:.v=.vo)
  79 VIFILES=$(VFILES:.v=.vi)
  80 GFILES=$(VFILES:.v=.g)
  81 HTMLFILES=$(VFILES:.v=.html)
  82 GHTMLFILES=$(VFILES:.v=.g.html)
  83
  84 all: st_base.vo\
  85   st_logic.vo\
  86   st_nat.vo\
  87   st_arith.vo\
  88   Standard.vo\
  89   xt_fin.vo\
  90   tbs_base.vo\
  91   tbs_rel.vo\
  92   tbs_op.vo\
  93   tbs_rop.vo\
  94   tbs_fun.vo\
  95   tbs_fin.vo\
  96   Toolbox.vo
  97
  98 spec: $(VIFILES)
  99
 100 gallina: $(GFILES)
 101
 102 html: $(HTMLFILES)
 103
 104 gallinahtml: $(GHTMLFILES)
 105
 106 all.ps: $(VFILES)
 107         $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
 108
 109 all-gal.ps: $(GFILES)
 110         $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`
 111
 112 xml:: .xml_time_stamp
 113 .xml_time_stamp: st_base.vo\
 114   st_logic.vo\
 115   st_nat.vo\
 116   st_arith.vo\
 117   Standard.vo\
 118   xt_fin.vo\
 119   tbs_base.vo\
 120   tbs_rel.vo\
 121   tbs_op.vo\
 122   tbs_rop.vo\
 123   tbs_fun.vo\
 124   tbs_fin.vo\
 125   Toolbox.vo
 126         $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
 127         touch .xml_time_stamp
 128
 129 ####################
 130 #                  #
 131 # Special targets. #
 132 #                  #
 133 ####################
 134
 135 .PHONY: all opt byte archclean clean install depend xml
 136
 137 .SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
 138
 139 .v.vo:
 140         $(COQC) $(COQDEBUG) $(COQFLAGS) $*
 141
 142 .v.vi:
 143         $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
 144
 145 .v.g:
 146         $(GALLINA) $<
 147
 148 .v.tex:
 149         $(COQWEB) $< -o $@
 150
 151 .v.html:
 152         $(COQWEB) -html $< -o $@
 153
 154 .g.g.tex:
 155         $(COQWEB) $< -o $@
 156
 157 .g.g.html:
 158         $(COQWEB) -html $< -o $@
 159
 160 byte:
 161         $(MAKE) all "OPT="
 162
 163 opt:
 164         $(MAKE) all "OPT=-opt"
 165
 166 include .depend
 167
 168 depend:
 169         rm .depend
 170         $(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
 171         $(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
 172
 173 xml::
 174
 175 install:
 176         mkdir -p `$(COQC) -where`/user-contrib
 177         cp -f *.vo `$(COQC) -where`/user-contrib
 178
 179 Makefile: Make
 180         mv -f Makefile Makefile.bak
 181         $(COQBIN)coq_makefile -f Make -o Makefile
 182
 183 clean:
 184         rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~
 185         rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
 186
 187 archclean:
 188         rm -f *.cmx *.o
 189
 190 # WARNING
 191 #
 192 # This Makefile has been automagically generated by coq_makefile
 193 # Edit at your own risks !
 194 #
 195 # END OF WARNING
 196