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

#
# This Makefile was generated by the command line :
# coq_makefile CompletePreorder.v ExtractionConsts.v FixedPoint.v FlatCompletePreorder.v Minimisation.v Preorder.v fact.v perfsqrt.v 
#

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

COQC=$(shell which coqc)
COQBIN=$(dir ${COQC})
COQTOP=`$(COQC) -where`
CAMLP4LIB=`camlp5 -where 2> /dev/null || camlp4 -where`
CAMLP4=`basename "$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)
GALLINA=gallina
COQDOC=$(COQBIN)/coqdoc
CAMLC=ocamlc -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"

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

OCAMLLIBS=-I .
COQLIBS=-I .

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

VFILES=CompletePreorder.v\
  ExtractionConsts.v\
  FixedPoint.v\
  FlatCompletePreorder.v\
  Minimisation.v\
  Preorder.v\
  fact.v\
  perfsqrt.v
VOFILES=$(VFILES:.v=.vo)
VIFILES=$(VFILES:.v=.vi)
GFILES=$(VFILES:.v=.g)
HTMLFILES=$(VFILES:.v=.html)
GHTMLFILES=$(VFILES:.v=.g.html)

all: CompletePreorder.vo\
  ExtractionConsts.vo\
  FixedPoint.vo\
  FlatCompletePreorder.vo\
  Minimisation.vo\
  Preorder.vo\
  fact.vo\
  perfsqrt.vo\
  fact\
  perfsqrt

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=-byte"

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

#
# OCaml targets
#

fact: fact.cmo fact-context.ml
	$(CAMLLINK) -o fact fact.cmo fact-context.ml

fact.cmo: fact.ml
	rm -f fact.mli
	$(CAMLC) -c fact.ml

fact.ml: fact.vo

perfsqrt: perfsqrt.cmo perfsqrt-context.ml
	$(CAMLLINK) -o perfsqrt perfsqrt.cmo perfsqrt-context.ml

perfsqrt.cmo: perfsqrt.ml
	rm -f perfsqrt.mli
	$(CAMLC) perfsqrt.ml

perfsqrt.ml: perfsqrt.vo


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

clean:
	rm -f fact.ml perfsqrt.ml
	rm -f *.mli *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~ .depend
	rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES) coqdoc.css

archclean:
	rm -f *.cmx *.o

html:

distro:
	tar -czf CompletePreorders.tgz $(VFILES) perfsqrt-context.ml fact-context.ml Makefile README