#########################################################################
##  v      #                  The Coq Proof Assistant                   ##
## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
##   \VV/  #                                                            ##
##    //   #   Makefile automagically generated by coq_makefile V8.1    ##
##########################################################################

# WARNING
#
# This Makefile has been automagically generated
# 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=$(shell camlp5 -where 2> /dev/null || camlp4 -where)
CAMLP4=$(notdir $(CAMLP4LIB))
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=$(COQBIN)gallina
COQDOC=$(COQBIN)coqdoc
CAMLC=ocamlc -rectypes -c
CAMLOPTC=ocamlopt -c
CAMLLINK=ocamlc
CAMLOPTLINK=ocamlopt
COQDEP=$(COQBIN)coqdep -c
GRAMMARS=grammar.cma
CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo
PP=-pp "$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl"
OTHERFLAGS=-dump-glob globals.dump

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

OCAMLLIBS=-I .
COQLIBS=-R . Lambda

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

VFILES=Utils.v\
  Tactics.v\
  MyList.v\
  ListType.v\
  Terms.v\
  LiftSubst.v\
  InvLiftSubst.v\
  Reduction.v\
  Conv.v\
  Conv_Dec.v\
  Hnf.v\
  Env.v\
  CCSum/Types.v\
  CCSum/Thinning.v\
  CCSum/Substitution.v\
  CCSum/Inversion.v\
  CCSum/TypeCase.v\
  CCSum/SubjectReduction.v\
  CCSum/Unicity.v\
  Russell/Types.v\
  Russell/Coercion.v\
  Russell/Inversion.v\
  Russell/Thinning.v\
  Russell/Substitution.v\
  Russell/GenerationNotKind.v\
  Russell/GenerationCoerce.v\
  Russell/Generation.v\
  Russell/GenerationRange.v\
  Russell/UnicityOfSortingRange.v\
  Russell/UnicityOfSorting.v\
  Russell/Injectivity.v\
  Russell/Depth.v\
  Russell/Narrowing.v\
  Russell/Transitivity.v\
  Russell/Inversion.v\
  Russell/SubjectReduction.v\
  Russell/Unicity.v\
  JRussell/Types.v\
  JRussell/Freevars.v\
  JRussell/Basic.v\
  JRussell/Conversion.v\
  JRussell/Coercion.v\
  JRussell/Thinning.v\
  JRussell/Substitution.v\
  JRussell/PreFunctionality.v\
  JRussell/Generation.v\
  JRussell/Validity.v\
  JRussell/GenerationNotKind.v\
  JRussell/GenerationCoerce.v\
  JRussell/GenerationRange.v\
  JRussell/UnicityOfSortingRange.v\
  JRussell/UnicityOfSorting.v\
  TPOSR/Terms.v\
  TPOSR/LiftSubst.v\
  TPOSR/Reduction.v\
  TPOSR/Conv.v\
  TPOSR/Conv_Dec.v\
  TPOSR/Env.v\
  TPOSR/Unlab.v\
  TPOSR/Types.v\
  TPOSR/Basic.v\
  TPOSR/UnicityOfSorting.v\
  TPOSR/MaxLemmas.v\
  TPOSR/TypesDepth.v\
  TPOSR/Thinning.v\
  TPOSR/CtxReduction.v\
  TPOSR/CtxExpansion.v\
  TPOSR/LeftReflexivity.v\
  TPOSR/Substitution.v\
  TPOSR/PreSubstitutionTPOSR.v\
  TPOSR/PreCtxCoercion.v\
  TPOSR/RightReflexivity.v\
  TPOSR/CtxConversion.v\
  TPOSR/CtxCoercion.v\
  TPOSR/SubstitutionTPOSR.v\
  TPOSR/Equiv.v\
  TPOSR/Generation.v\
  TPOSR/Validity.v\
  TPOSR/TypesFunctionality.v\
  TPOSR/UniquenessOfTypes.v\
  TPOSR/ChurchRosserDepth.v\
  TPOSR/ChurchRosser.v\
  TPOSR/CoerceDepth.v\
  TPOSR/CoerceNoTrans.v\
  TPOSR/TransitivitySet.v\
  TPOSR/Transitivity.v\
  TPOSR/Injectivity.v\
  TPOSR/SubjectReduction.v\
  TPOSR/TPOSR_trans.v\
  TPOSR/UnlabConv.v\
  Meta/JRussell_Russell.v\
  Meta/TPOSR_JRussell.v\
  Meta/TPOSR_Russell.v\
  Meta/Russell_TPOSR.v\
  Meta/Russell_JRussell.v\
  Meta/SubjectReduction.v\
  Russell./Types.v
VOFILES=$(VFILES:.v=.vo)
VIFILES=$(VFILES:.v=.vi)
GFILES=$(VFILES:.v=.g)
HTMLFILES=$(VFILES:.v=.html)
GHTMLFILES=$(VFILES:.v=.g.html)

all: Utils.vo\
  Tactics.vo\
  MyList.vo\
  ListType.vo\
  Terms.vo\
  LiftSubst.vo\
  InvLiftSubst.vo\
  Reduction.vo\
  Conv.vo\
  Conv_Dec.vo\
  Hnf.vo\
  Env.vo\
  CCSum/Types.vo\
  CCSum/Thinning.vo\
  CCSum/Substitution.vo\
  CCSum/Inversion.vo\
  CCSum/TypeCase.vo\
  CCSum/SubjectReduction.vo\
  CCSum/Unicity.vo\
  Russell/Types.vo\
  Russell/Coercion.vo\
  Russell/Inversion.vo\
  Russell/Thinning.vo\
  Russell/Substitution.vo\
  Russell/GenerationNotKind.vo\
  Russell/GenerationCoerce.vo\
  Russell/Generation.vo\
  Russell/GenerationRange.vo\
  Russell/UnicityOfSortingRange.vo\
  Russell/UnicityOfSorting.vo\
  Russell/Injectivity.vo\
  Russell/Depth.vo\
  Russell/Narrowing.vo\
  Russell/Transitivity.vo\
  Russell/Inversion.vo\
  Russell/SubjectReduction.vo\
  Russell/Unicity.vo\
  JRussell/Types.vo\
  JRussell/Freevars.vo\
  JRussell/Basic.vo\
  JRussell/Conversion.vo\
  JRussell/Coercion.vo\
  JRussell/Thinning.vo\
  JRussell/Substitution.vo\
  JRussell/PreFunctionality.vo\
  JRussell/Generation.vo\
  JRussell/Validity.vo\
  JRussell/GenerationNotKind.vo\
  JRussell/GenerationCoerce.vo\
  JRussell/GenerationRange.vo\
  JRussell/UnicityOfSortingRange.vo\
  JRussell/UnicityOfSorting.vo\
  TPOSR/Terms.vo\
  TPOSR/LiftSubst.vo\
  TPOSR/Reduction.vo\
  TPOSR/Conv.vo\
  TPOSR/Conv_Dec.vo\
  TPOSR/Env.vo\
  TPOSR/Unlab.vo\
  TPOSR/Types.vo\
  TPOSR/Basic.vo\
  TPOSR/UnicityOfSorting.vo\
  TPOSR/MaxLemmas.vo\
  TPOSR/TypesDepth.vo\
  TPOSR/Thinning.vo\
  TPOSR/CtxReduction.vo\
  TPOSR/CtxExpansion.vo\
  TPOSR/LeftReflexivity.vo\
  TPOSR/Substitution.vo\
  TPOSR/PreSubstitutionTPOSR.vo\
  TPOSR/PreCtxCoercion.vo\
  TPOSR/RightReflexivity.vo\
  TPOSR/CtxConversion.vo\
  TPOSR/CtxCoercion.vo\
  TPOSR/SubstitutionTPOSR.vo\
  TPOSR/Equiv.vo\
  TPOSR/Generation.vo\
  TPOSR/Validity.vo\
  TPOSR/TypesFunctionality.vo\
  TPOSR/UniquenessOfTypes.vo\
  TPOSR/ChurchRosserDepth.vo\
  TPOSR/ChurchRosser.vo\
  TPOSR/CoerceDepth.vo\
  TPOSR/CoerceNoTrans.vo\
  TPOSR/TransitivitySet.vo\
  TPOSR/Transitivity.vo\
  TPOSR/Injectivity.vo\
  TPOSR/SubjectReduction.vo\
  TPOSR/TPOSR_trans.vo\
  TPOSR/UnlabConv.vo\
  Meta/JRussell_Russell.vo\
  Meta/TPOSR_JRussell.vo\
  Meta/TPOSR_Russell.vo\
  Meta/Russell_TPOSR.vo\
  Meta/Russell_JRussell.vo\
  Meta/SubjectReduction.vo\
  Russell./Types.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

%.vo %.glob: %.v
	$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*

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

%.g: %.v
	$(GALLINA) $<

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

%.html: %.v %.glob
	$(COQDOC) -glob-from $*.glob  -html $< -o $@

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

%.g.html: %.v %.glob
	$(COQDOC) -glob-from $*.glob -html -g $< -o $@

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

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

include .depend

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

install:
	mkdir -p `$(COQC) -where`/user-contrib
	cp -f $(VOFILES) `$(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 $(VOFILES) $(VIFILES) $(GFILES) *~
	rm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex)

archclean:
	rm -f *.cmx *.o

html:

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