##############################################################################
##                 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 -I basis/ -I list_extensions -I term_algebra -I term_orderings -I ac_matching -I unification basis/closure.v basis/decidable_set.v basis/ordered_set.v list_extensions/dickson.v list_extensions/equiv_list.v list_extensions/list_permut.v list_extensions/list_set.v list_extensions/list_sort.v list_extensions/more_list.v term_algebra/equational_theory.v term_algebra/term.v term_orderings/rpo.v term_orderings/term_o.v ac_matching/ac.v ac_matching/cf_eq_ac.v ac_matching/matching_algo.v ac_matching/matching_complete.v ac_matching/matching_sound.v ac_matching/matching.v ac_matching/matching_well_formed.v ac_matching/matching_well_founded.v unification/free_unif.v unification/unification.v -custom rm -f doc/*.html; $(COQDOC) --glob-from doc/glob -d doc \
   	$(VFILES) $(VFILES) docu 
#

##########################
#                        #
# 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 -dump-glob doc/glob
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_ifdef.cmo q_MLast.cmo
PP=-pp "camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl"

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

OCAMLLIBS=-I .\
  -I basis/\
  -I list_extensions\
  -I term_algebra\
  -I term_orderings\
  -I ac_matching\
  -I unification
COQLIBS=-I .\
  -I basis/\
  -I list_extensions\
  -I term_algebra\
  -I term_orderings\
  -I ac_matching\
  -I unification

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

VFILES=basis/closure.v\
  basis/decidable_set.v\
  basis/ordered_set.v\
  list_extensions/dickson.v\
  list_extensions/equiv_list.v\
  list_extensions/list_permut.v\
  list_extensions/list_set.v\
  list_extensions/list_sort.v\
  list_extensions/more_list.v\
  term_algebra/equational_theory.v\
  term_algebra/term.v\
  term_orderings/rpo.v\
  term_orderings/term_o.v\
  ac_matching/ac.v\
  ac_matching/cf_eq_ac.v\
  ac_matching/matching_algo.v\
  ac_matching/matching_complete.v\
  ac_matching/matching_sound.v\
  ac_matching/matching.v\
  ac_matching/matching_well_formed.v\
  ac_matching/matching_well_founded.v\
  unification/free_unif.v\
  unification/unification.v
VOFILES=$(VFILES:.v=.vo)
VIFILES=$(VFILES:.v=.vi)
GFILES=$(VFILES:.v=.g)
HTMLFILES=$(VFILES:.v=.html)
GHTMLFILES=$(VFILES:.v=.g.html)

all: basis/closure.vo\
  basis/decidable_set.vo\
  basis/ordered_set.vo\
  list_extensions/dickson.vo\
  list_extensions/equiv_list.vo\
  list_extensions/list_permut.vo\
  list_extensions/list_set.vo\
  list_extensions/list_sort.vo\
  list_extensions/more_list.vo\
  term_algebra/equational_theory.vo\
  term_algebra/term.vo\
  term_orderings/rpo.vo\
  term_orderings/term_o.vo\
  ac_matching/ac.vo\
  ac_matching/cf_eq_ac.vo\
  ac_matching/matching_algo.vo\
  ac_matching/matching_complete.vo\
  ac_matching/matching_sound.vo\
  ac_matching/matching.vo\
  ac_matching/matching_well_formed.vo\
  ac_matching/matching_well_founded.vo\
  unification/free_unif.vo\
  unification/unification.vo\
  docu

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)`



###################
#                 #
# Custom targets. #
#                 #
###################

docu: $(VFILES)
	rm -f doc/*.html; $(COQDOC) --glob-from doc/glob -d doc \
   	$(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) $(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 *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~
	rm -f doc/glob all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
	- rm -f docu

archclean:
	rm -f *.cmx *.o

html:

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