################################################################################                 The Calculus of Inductive Constructions                  ####                                                                          ####                                Projet Coq                                ####                                                                          ####                     INRIA                        ENS-CNRS                ####              Rocquencourt                        Lyon                    ####                                                                          ####                                  Coq V7                                  ####                                                                          ####                                                                          ################################################################################# WARNING
#
# This Makefile has been automagically generated by coq_makefile
# Edit at your own risks !
#
# END OF WARNING

#
# This Makefile was generated by the command line :
# coq_makefile chap6.v seasons.v boolequal.v exobool.v partialfunc.v lt_3.v more_seasons.v month.v pos_even_bool.v mult2.v rplus.v exo_sum_f.v sum.v Rat_prelude.v Rat.v bool_discr.v man_inj.v two_power.v binary_word_or.v binary_word.v emptyset.v manhattan.v height.v nbseats.v positive.v vectors.v propositional.v first_in_list.v is_January.v fzero_present.v tree_bij.v erato.v depfun.v exo_frac.v pos_div4.v power_log.v plus_n_O.v value_present.v poly_tree.v twofirst.v iota.v nth_option.v nth_length.v first_in_list.v split.v izero_present.v 
#

##########################
#                        #
# Variables definitions. #
#                        #
##########################

CAMLP4LIB=`camlp4 -where`
COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \  -I $(COQTOP)/library -I $(COQTOP)/parsing \  -I $(COQTOP)/pretyping -I $(COQTOP)/interp \  -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \  -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \  -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \  -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \  -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \  -I $(CAMLP4LIB)
ZFLAGS=$(OCAMLLIBS) $(COQSRC)
OPT=
COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQC=$(COQBIN)coqc
GALLINA=gallina
COQDOC=coqdoc
CAMLC=ocamlc -c
CAMLOPTC=ocamlopt -c
CAMLLINK=ocamlc
CAMLOPTLINK=ocamlopt
COQDEP=$(COQBIN)coqdep -c
GRAMMARS=grammar.cma
CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo
PP=-pp "camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl"

#########################
#                       #
# Libraries definition. #
#                       #
#########################

OCAMLLIBS=-I .
COQLIBS=-I .

###################################
#                                 #
# Definition of the "all" target. #
#                                 #
###################################

VFILES=chap6.v\
  seasons.v\
  boolequal.v\
  exobool.v\
  partialfunc.v\
  lt_3.v\
  more_seasons.v\
  month.v\
  pos_even_bool.v\
  mult2.v\
  rplus.v\
  exo_sum_f.v\
  sum.v\
  Rat_prelude.v\
  Rat.v\
  bool_discr.v\
  man_inj.v\
  two_power.v\
  binary_word_or.v\
  binary_word.v\
  emptyset.v\
  manhattan.v\
  height.v\
  nbseats.v\
  positive.v\
  vectors.v\
  propositional.v\
  first_in_list.v\
  is_January.v\
  fzero_present.v\
  tree_bij.v\
  erato.v\
  depfun.v\
  exo_frac.v\
  pos_div4.v\
  power_log.v\
  plus_n_O.v\
  value_present.v\
  poly_tree.v\
  twofirst.v\
  iota.v\
  nth_option.v\
  nth_length.v\
  first_in_list.v\
  split.v\
  izero_present.v
VOFILES=$(VFILES:.v=.vo)
VIFILES=$(VFILES:.v=.vi)
GFILES=$(VFILES:.v=.g)
HTMLFILES=$(VFILES:.v=.html)
GHTMLFILES=$(VFILES:.v=.g.html)

all: chap6.vo\
  seasons.vo\
  boolequal.vo\
  exobool.vo\
  partialfunc.vo\
  lt_3.vo\
  more_seasons.vo\
  month.vo\
  pos_even_bool.vo\
  mult2.vo\
  rplus.vo\
  exo_sum_f.vo\
  sum.vo\
  Rat_prelude.vo\
  Rat.vo\
  bool_discr.vo\
  man_inj.vo\
  two_power.vo\
  binary_word_or.vo\
  binary_word.vo\
  emptyset.vo\
  manhattan.vo\
  height.vo\
  nbseats.vo\
  positive.vo\
  vectors.vo\
  propositional.vo\
  first_in_list.vo\
  is_January.vo\
  fzero_present.vo\
  tree_bij.vo\
  erato.vo\
  depfun.vo\
  exo_frac.vo\
  pos_div4.vo\
  power_log.vo\
  plus_n_O.vo\
  value_present.vo\
  poly_tree.vo\
  twofirst.vo\
  iota.vo\
  nth_option.vo\
  nth_length.vo\
  first_in_list.vo\
  split.vo\
  izero_present.vo

spec: $(VIFILES)

gallina: $(GFILES)

html: $(HTMLFILES)

gallinahtml: $(GHTMLFILES)

all.ps: $(VFILES)
	$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`

all-gal.ps: $(VFILES)
	$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`



####################
#                  #
# Special targets. #
#                  #
####################

.PHONY: all opt byte archclean clean install depend html

.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html

.v.vo:
	$(COQC) $(COQDEBUG) $(COQFLAGS) $*

.v.vi:
	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*

.v.g:
	$(GALLINA) $<

.v.tex:
	$(COQDOC) -latex $< -o $@

.v.html:
	$(COQDOC) -html $< -o $@

.v.g.tex:
	$(COQDOC) -latex -g $< -o $@

.v.g.html:
	$(COQDOC) -html -g $< -o $@

byte:
	$(MAKE) all "OPT="

opt:
	$(MAKE) all "OPT=-opt"

include .depend

.depend depend:
	rm -f .depend
	$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
	$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend

install:
	mkdir -p `$(COQC) -where`/user-contrib
	cp -f *.vo `$(COQC) -where`/user-contrib

clean:
	rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~
	rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)

archclean:
	rm -f *.cmx *.o

html:

# WARNING
#
# This Makefile has been automagically generated by coq_makefile
# Edit at your own risks !
#
# END OF WARNING

