helm/coq-contribs/LAMBDA-TYPES/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=base_tactics.v\
  66   base_hints.v\
  67   base_types.v\
  68   base_blt.v\
  69   base_rewrite.v\
  70   Base.v\
  71   terms_defs.v\
  72   tlt_defs.v\
  73   contexts_defs.v\
  74   lift_defs.v\
  75   lift_gen.v\
  76   lift_props.v\
  77   lift_tlt.v\
  78   drop_defs.v\
  79   drop_props.v\
  80   subst0_defs.v\
  81   subst0_gen.v\
  82   subst0_lift.v\
  83   subst0_subst0.v\
  84   subst0_confluence.v\
  85   subst0_tlt.v\
  86   subst1_defs.v\
  87   subst1_gen.v\
  88   subst1_lift.v\
  89   subst1_subst1.v\
  90   subst1_confluence.v\
  91   csubst0_defs.v\
  92   csubst1_defs.v\
  93   fsubst0_defs.v\
  94   pr0_defs.v\
  95   pr0_lift.v\
  96   pr0_gen.v\
  97   pr0_subst0.v\
  98   pr0_confluence.v\
  99   pr0_subst1.v\
 100   pr1_defs.v\
 101   pr1_confluence.v\
 102   cpr0_defs.v\
 103   pr2_defs.v\
 104   pr2_lift.v\
 105   pr2_gen.v\
 106   pr2_confluence.v\
 107   pr2_subst1.v\
 108   pr2_gen_context.v\
 109   pr3_defs.v\
 110   pr3_props.v\
 111   pr3_gen.v\
 112   pr3_confluence.v\
 113   pr3_subst1.v\
 114   pr3_gen_context.v\
 115   pc1_defs.v\
 116   pc1_props.v\
 117   pc3_defs.v\
 118   pc3_props.v\
 119   pc3_gen.v\
 120   pc3_subst0.v\
 121   pc3_gen_context.v\
 122   ty0_defs.v\
 123   ty0_gen.v\
 124   ty0_lift.v\
 125   ty0_props.v\
 126   ty0_subst0.v\
 127   ty0_gen_context.v\
 128   csub0_defs.v\
 129   csub0_props.v\
 130   ty0_sred.v\
 131   ty0_sred_props.v\
 132   LambdaDelta.v
 133 VOFILES=$(VFILES:.v=.vo)
 134 VIFILES=$(VFILES:.v=.vi)
 135 GFILES=$(VFILES:.v=.g)
 136 HTMLFILES=$(VFILES:.v=.html)
 137 GHTMLFILES=$(VFILES:.v=.g.html)
 138
 139 all: base_tactics.vo\
 140   base_hints.vo\
 141   base_types.vo\
 142   base_blt.vo\
 143   base_rewrite.vo\
 144   Base.vo\
 145   terms_defs.vo\
 146   tlt_defs.vo\
 147   contexts_defs.vo\
 148   lift_defs.vo\
 149   lift_gen.vo\
 150   lift_props.vo\
 151   lift_tlt.vo\
 152   drop_defs.vo\
 153   drop_props.vo\
 154   subst0_defs.vo\
 155   subst0_gen.vo\
 156   subst0_lift.vo\
 157   subst0_subst0.vo\
 158   subst0_confluence.vo\
 159   subst0_tlt.vo\
 160   subst1_defs.vo\
 161   subst1_gen.vo\
 162   subst1_lift.vo\
 163   subst1_subst1.vo\
 164   subst1_confluence.vo\
 165   csubst0_defs.vo\
 166   csubst1_defs.vo\
 167   fsubst0_defs.vo\
 168   pr0_defs.vo\
 169   pr0_lift.vo\
 170   pr0_gen.vo\
 171   pr0_subst0.vo\
 172   pr0_confluence.vo\
 173   pr0_subst1.vo\
 174   pr1_defs.vo\
 175   pr1_confluence.vo\
 176   cpr0_defs.vo\
 177   pr2_defs.vo\
 178   pr2_lift.vo\
 179   pr2_gen.vo\
 180   pr2_confluence.vo\
 181   pr2_subst1.vo\
 182   pr2_gen_context.vo\
 183   pr3_defs.vo\
 184   pr3_props.vo\
 185   pr3_gen.vo\
 186   pr3_confluence.vo\
 187   pr3_subst1.vo\
 188   pr3_gen_context.vo\
 189   pc1_defs.vo\
 190   pc1_props.vo\
 191   pc3_defs.vo\
 192   pc3_props.vo\
 193   pc3_gen.vo\
 194   pc3_subst0.vo\
 195   pc3_gen_context.vo\
 196   ty0_defs.vo\
 197   ty0_gen.vo\
 198   ty0_lift.vo\
 199   ty0_props.vo\
 200   ty0_subst0.vo\
 201   ty0_gen_context.vo\
 202   csub0_defs.vo\
 203   csub0_props.vo\
 204   ty0_sred.vo\
 205   ty0_sred_props.vo\
 206   LambdaDelta.vo
 207
 208 spec: $(VIFILES)
 209
 210 gallina: $(GFILES)
 211
 212 html: $(HTMLFILES)
 213
 214 gallinahtml: $(GHTMLFILES)
 215
 216 all.ps: $(VFILES)
 217         $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
 218
 219 all-gal.ps: $(GFILES)
 220         $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`
 221
 222 xml:: .xml_time_stamp
 223 .xml_time_stamp: base_tactics.vo\
 224   base_hints.vo\
 225   base_types.vo\
 226   base_blt.vo\
 227   base_rewrite.vo\
 228   Base.vo\
 229   terms_defs.vo\
 230   tlt_defs.vo\
 231   contexts_defs.vo\
 232   lift_defs.vo\
 233   lift_gen.vo\
 234   lift_props.vo\
 235   lift_tlt.vo\
 236   drop_defs.vo\
 237   drop_props.vo\
 238   subst0_defs.vo\
 239   subst0_gen.vo\
 240   subst0_lift.vo\
 241   subst0_subst0.vo\
 242   subst0_confluence.vo\
 243   subst0_tlt.vo\
 244   subst1_defs.vo\
 245   subst1_gen.vo\
 246   subst1_lift.vo\
 247   subst1_subst1.vo\
 248   subst1_confluence.vo\
 249   csubst0_defs.vo\
 250   csubst1_defs.vo\
 251   fsubst0_defs.vo\
 252   pr0_defs.vo\
 253   pr0_lift.vo\
 254   pr0_gen.vo\
 255   pr0_subst0.vo\
 256   pr0_confluence.vo\
 257   pr0_subst1.vo\
 258   pr1_defs.vo\
 259   pr1_confluence.vo\
 260   cpr0_defs.vo\
 261   pr2_defs.vo\
 262   pr2_lift.vo\
 263   pr2_gen.vo\
 264   pr2_confluence.vo\
 265   pr2_subst1.vo\
 266   pr2_gen_context.vo\
 267   pr3_defs.vo\
 268   pr3_props.vo\
 269   pr3_gen.vo\
 270   pr3_confluence.vo\
 271   pr3_subst1.vo\
 272   pr3_gen_context.vo\
 273   pc1_defs.vo\
 274   pc1_props.vo\
 275   pc3_defs.vo\
 276   pc3_props.vo\
 277   pc3_gen.vo\
 278   pc3_subst0.vo\
 279   pc3_gen_context.vo\
 280   ty0_defs.vo\
 281   ty0_gen.vo\
 282   ty0_lift.vo\
 283   ty0_props.vo\
 284   ty0_subst0.vo\
 285   ty0_gen_context.vo\
 286   csub0_defs.vo\
 287   csub0_props.vo\
 288   ty0_sred.vo\
 289   ty0_sred_props.vo\
 290   LambdaDelta.vo
 291         $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
 292         touch .xml_time_stamp
 293
 294 ####################
 295 #                  #
 296 # Special targets. #
 297 #                  #
 298 ####################
 299
 300 .PHONY: all opt byte archclean clean install depend xml
 301
 302 .SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
 303
 304 .v.vo:
 305         $(COQC) $(COQDEBUG) $(COQFLAGS) $*
 306
 307 .v.vi:
 308         $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
 309
 310 .v.g:
 311         $(GALLINA) $<
 312
 313 .v.tex:
 314         $(COQWEB) $< -o $@
 315
 316 .v.html:
 317         $(COQWEB) -html $< -o $@
 318
 319 .g.g.tex:
 320         $(COQWEB) $< -o $@
 321
 322 .g.g.html:
 323         $(COQWEB) -html $< -o $@
 324
 325 byte:
 326         $(MAKE) all "OPT="
 327
 328 opt:
 329         $(MAKE) all "OPT=-opt"
 330
 331 include .depend
 332
 333 depend:
 334         rm .depend
 335         $(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
 336         $(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
 337
 338 xml::
 339
 340 install:
 341         mkdir -p `$(COQC) -where`/user-contrib
 342         cp -f *.vo `$(COQC) -where`/user-contrib
 343
 344 Makefile: Make
 345         mv -f Makefile Makefile.bak
 346         $(COQBIN)coq_makefile -f Make -o Makefile
 347
 348 clean:
 349         rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~
 350         rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
 351
 352 archclean:
 353         rm -f *.cmx *.o
 354
 355 # WARNING
 356 #
 357 # This Makefile has been automagically generated by coq_makefile
 358 # Edit at your own risks !
 359 #
 360 # END OF WARNING
 361