##############################################################################
##                 The Calculus of Inductive Constructions                  ##
##                                                                          ##
##                                Projet Coq                                ##
##                                                                          ##
##                     INRIA                        ENS-CNRS                ##
##              Rocquencourt                        Lyon                    ##
##                                                                          ##
##                                Coq V6.1                                  ##
##                                                                          ##
##                                                                          ##
##############################################################################

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

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

MAKE=make "COQBIN=$(COQBIN)" "OPT=$(OPT)"
COQSRC=-I $(COQTOP)/src/tactics -I $(COQTOP)/src/proofs \
  -I $(COQTOP)/src/syntax -I $(COQTOP)/src/env -I $(COQTOP)/src/lib/util \
  -I $(COQTOP)/src/constr -I $(COQTOP)/tactics -I $(COQTOP)/src/meta
ZFLAGS=$(LIBS) $(COQSRC)
FULLOPT=$(OPT:-opt=-full)
COQFLAGS=-q $(OPT) $(LIBS)
COQC=$(COQBIN)coqc
COQFULL=$(COQBIN)coqc $(FULLOPT) -q $(LIBS)
CAMLC=ocamlc -c
CAMLOPT=ocamlopt -c
CAMLLINK=ocamlc
CAMLOPTLINK=ocamlopt
COQDEP=$(COQBIN)coqdep -c

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

LIBS=-I .

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

all:: MinMJ_Bridge.vo\
  MinMJ_Bridge2.vo\
  MinMJ_Bridge3.vo\
  MinMJ_Drop.vo\
  MinMJ_Exchange.vo\
  MinMJ_Exchange2.vo\
  MinMJ_Exchange3.vo\
  MinMJ_F.vo\
  MinMJ_HeightL.vo\
  MinMJ_HeightM.vo\
  MinMJ_Hyps.vo\
  MinMJ_In.vo\
  MinMJ_L.vo\
  MinMJ_LJ.vo\
  MinMJ_LMN.vo\
  MinMJ_L_Admis_RhoBar.vo\
  MinMJ_Lift.vo\
  MinMJ_Lifts.vo\
  MinMJ_M.vo\
  MinMJ_MJ.vo\
  MinMJ_M_Admis_Psi.vo\
  MinMJ_Main.vo\
  MinMJ_Msub.vo\
  MinMJ_N.vo\
  MinMJ_NJ.vo\
  MinMJ_N_Admis_Phi.vo\
  MinMJ_N_Admis_Theta.vo\
  MinMJ_NormL.vo\
  MinMJ_Normal_Perm.vo\
  MinMJ_Normal_RhoBar.vo\
  MinMJ_Nsub.vo\
  MinMJ_Occurs.vo\
  MinMJ_Occurs_Lift.vo\
  MinMJ_PermDef.vo\
  MinMJ_Strength.vo\
  MinMJ_Syntax.vo\
  MinMJ_Weak.vo\
  MinMJ_booleans.vo\
  MinMJ_lt.vo\
  MinMJ_nat.vo\
  MinMJ_phi.vo\
  MinMJ_phibar.vo\
  MinMJ_psi.vo\
  MinMJ_psitheta.vo\
  MinMJ_rhobar.vo\
  MinMJ_theta.vo\
  MinMJ_thetapsi.vo\
  autocontra.vo\
  autocontra.cmo

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

.PHONY: all opt byte archclean clean depend

.SUFFIXES: .mli .ml .cmo .cmi .v .vo

.mli.cmi:
	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<

.ml.cmo:
	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<

.ml.cmx:
	$(CAMLOPT) $(ZDEBUG) $(ZFLAGS) $<

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

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

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

include .depend

depend::
	rm .depend
	$(COQDEP) $(LIBS) *.v *.ml *.mli >.depend

clean::
	rm -f *.cmo *.cmi *.cmx *.vo *~

archclean::
	rm -f *.cmx

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