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