##############################################################################
##                 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 -f Make -o Makefile 
#

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

CAMLP4LIB=`camlp4 -where`
COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
  -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
  -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
  -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
ZFLAGS=$(OCAMLLIBS) $(COQSRC)
OPT=
COQFLAGS=-q $(OPT) $(COQLIBS)
COQC=$(COQBIN)coqc
GALLINA=gallina
COQWEB=coqweb
CAMLC=ocamlc -c
CAMLOPTC=ocamlopt -c
CAMLLINK=ocamlc
CAMLOPTLINK=ocamlopt
COQDEP=$(COQBIN)coqdep -c
COQVO2XML=coq_vo2xml

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

OCAMLLIBS=-I .
COQLIBS=-I .

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

VFILES=base_tactics.v\
  base_hints.v\
  base_types.v\
  base_blt.v\
  base_rewrite.v\
  Base.v\
  terms_defs.v\
  tlt_defs.v\
  contexts_defs.v\
  lift_defs.v\
  lift_gen.v\
  lift_props.v\
  lift_tlt.v\
  drop_defs.v\
  drop_props.v\
  subst0_defs.v\
  subst0_gen.v\
  subst0_lift.v\
  subst0_subst0.v\
  subst0_confluence.v\
  subst0_tlt.v\
  subst1_defs.v\
  subst1_gen.v\
  subst1_lift.v\
  subst1_subst1.v\
  subst1_confluence.v\
  csubst0_defs.v\
  csubst1_defs.v\
  fsubst0_defs.v\
  pr0_defs.v\
  pr0_lift.v\
  pr0_gen.v\
  pr0_subst0.v\
  pr0_confluence.v\
  pr0_subst1.v\
  pr1_defs.v\
  pr1_confluence.v\
  cpr0_defs.v\
  pr2_defs.v\
  pr2_lift.v\
  pr2_gen.v\
  pr2_confluence.v\
  pr2_subst1.v\
  pr2_gen_context.v\
  pr3_defs.v\
  pr3_props.v\
  pr3_gen.v\
  pr3_confluence.v\
  pr3_subst1.v\
  pr3_gen_context.v\
  pc1_defs.v\
  pc1_props.v\
  pc3_defs.v\
  pc3_props.v\
  pc3_gen.v\
  pc3_subst0.v\
  pc3_gen_context.v\
  ty0_defs.v\
  ty0_gen.v\
  ty0_lift.v\
  ty0_props.v\
  ty0_subst0.v\
  ty0_gen_context.v\
  csub0_defs.v\
  csub0_props.v\
  ty0_sred.v\
  ty0_sred_props.v\
  LambdaDelta.v
VOFILES=$(VFILES:.v=.vo)
VIFILES=$(VFILES:.v=.vi)
GFILES=$(VFILES:.v=.g)
HTMLFILES=$(VFILES:.v=.html)
GHTMLFILES=$(VFILES:.v=.g.html)

all: base_tactics.vo\
  base_hints.vo\
  base_types.vo\
  base_blt.vo\
  base_rewrite.vo\
  Base.vo\
  terms_defs.vo\
  tlt_defs.vo\
  contexts_defs.vo\
  lift_defs.vo\
  lift_gen.vo\
  lift_props.vo\
  lift_tlt.vo\
  drop_defs.vo\
  drop_props.vo\
  subst0_defs.vo\
  subst0_gen.vo\
  subst0_lift.vo\
  subst0_subst0.vo\
  subst0_confluence.vo\
  subst0_tlt.vo\
  subst1_defs.vo\
  subst1_gen.vo\
  subst1_lift.vo\
  subst1_subst1.vo\
  subst1_confluence.vo\
  csubst0_defs.vo\
  csubst1_defs.vo\
  fsubst0_defs.vo\
  pr0_defs.vo\
  pr0_lift.vo\
  pr0_gen.vo\
  pr0_subst0.vo\
  pr0_confluence.vo\
  pr0_subst1.vo\
  pr1_defs.vo\
  pr1_confluence.vo\
  cpr0_defs.vo\
  pr2_defs.vo\
  pr2_lift.vo\
  pr2_gen.vo\
  pr2_confluence.vo\
  pr2_subst1.vo\
  pr2_gen_context.vo\
  pr3_defs.vo\
  pr3_props.vo\
  pr3_gen.vo\
  pr3_confluence.vo\
  pr3_subst1.vo\
  pr3_gen_context.vo\
  pc1_defs.vo\
  pc1_props.vo\
  pc3_defs.vo\
  pc3_props.vo\
  pc3_gen.vo\
  pc3_subst0.vo\
  pc3_gen_context.vo\
  ty0_defs.vo\
  ty0_gen.vo\
  ty0_lift.vo\
  ty0_props.vo\
  ty0_subst0.vo\
  ty0_gen_context.vo\
  csub0_defs.vo\
  csub0_props.vo\
  ty0_sred.vo\
  ty0_sred_props.vo\
  LambdaDelta.vo

spec: $(VIFILES)

gallina: $(GFILES)

html: $(HTMLFILES)

gallinahtml: $(GHTMLFILES)

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

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

xml:: .xml_time_stamp
.xml_time_stamp: base_tactics.vo\
  base_hints.vo\
  base_types.vo\
  base_blt.vo\
  base_rewrite.vo\
  Base.vo\
  terms_defs.vo\
  tlt_defs.vo\
  contexts_defs.vo\
  lift_defs.vo\
  lift_gen.vo\
  lift_props.vo\
  lift_tlt.vo\
  drop_defs.vo\
  drop_props.vo\
  subst0_defs.vo\
  subst0_gen.vo\
  subst0_lift.vo\
  subst0_subst0.vo\
  subst0_confluence.vo\
  subst0_tlt.vo\
  subst1_defs.vo\
  subst1_gen.vo\
  subst1_lift.vo\
  subst1_subst1.vo\
  subst1_confluence.vo\
  csubst0_defs.vo\
  csubst1_defs.vo\
  fsubst0_defs.vo\
  pr0_defs.vo\
  pr0_lift.vo\
  pr0_gen.vo\
  pr0_subst0.vo\
  pr0_confluence.vo\
  pr0_subst1.vo\
  pr1_defs.vo\
  pr1_confluence.vo\
  cpr0_defs.vo\
  pr2_defs.vo\
  pr2_lift.vo\
  pr2_gen.vo\
  pr2_confluence.vo\
  pr2_subst1.vo\
  pr2_gen_context.vo\
  pr3_defs.vo\
  pr3_props.vo\
  pr3_gen.vo\
  pr3_confluence.vo\
  pr3_subst1.vo\
  pr3_gen_context.vo\
  pc1_defs.vo\
  pc1_props.vo\
  pc3_defs.vo\
  pc3_props.vo\
  pc3_gen.vo\
  pc3_subst0.vo\
  pc3_gen_context.vo\
  ty0_defs.vo\
  ty0_gen.vo\
  ty0_lift.vo\
  ty0_props.vo\
  ty0_subst0.vo\
  ty0_gen_context.vo\
  csub0_defs.vo\
  csub0_props.vo\
  ty0_sred.vo\
  ty0_sred_props.vo\
  LambdaDelta.vo
	$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
	touch .xml_time_stamp

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

.PHONY: all opt byte archclean clean install depend xml

.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:
	$(COQWEB) $< -o $@

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

.g.g.tex:
	$(COQWEB) $< -o $@

.g.g.html:
	$(COQWEB) -html $< -o $@

byte:
	$(MAKE) all "OPT="

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

include .depend

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

xml::

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

Makefile: Make
	mv -f Makefile Makefile.bak
	$(COQBIN)coq_makefile -f Make -o Makefile

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

archclean:
	rm -f *.cmx *.o

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