##############################################################################
##                 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
COQ2HTML=coq2html
COQ2LATEX=coq2latex
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. #
#                                 #
###################################

all: Params.vo\
  EqParams.vo\
  NSyntax.vo\
  Axioms.vo\
  EqAxioms.vo\
  NeqParams.vo\
  NeqAxioms.vo\
  NeqDef.vo\
  NeqProps.vo\
  AddProps.vo\
  LtProps.vo\
  OppProps.vo\
  SubProps.vo\
  LeAxioms.vo\
  LeProps.vo\
  GtAxioms.vo\
  GtProps.vo\
  GeAxioms.vo\
  GeProps.vo\
  DiscrAxioms.vo\
  DiscrProps.vo\
  OppAxioms.vo\
  Leibniz\
  Nat

spec: Params.vi\
  EqParams.vi\
  NSyntax.vi\
  Axioms.vi\
  EqAxioms.vi\
  NeqParams.vi\
  NeqAxioms.vi\
  NeqDef.vi\
  NeqProps.vi\
  AddProps.vi\
  LtProps.vi\
  OppProps.vi\
  SubProps.vi\
  LeAxioms.vi\
  LeProps.vi\
  GtAxioms.vi\
  GtProps.vi\
  GeAxioms.vi\
  GeProps.vi\
  DiscrAxioms.vi\
  DiscrProps.vi\
  OppAxioms.vi

gallina: Params.g\
  EqParams.g\
  NSyntax.g\
  Axioms.g\
  EqAxioms.g\
  NeqParams.g\
  NeqAxioms.g\
  NeqDef.g\
  NeqProps.g\
  AddProps.g\
  LtProps.g\
  OppProps.g\
  SubProps.g\
  LeAxioms.g\
  LeProps.g\
  GtAxioms.g\
  GtProps.g\
  GeAxioms.g\
  GeProps.g\
  DiscrAxioms.g\
  DiscrProps.g\
  OppAxioms.g

html: Params.html\
  EqParams.html\
  NSyntax.html\
  Axioms.html\
  EqAxioms.html\
  NeqParams.html\
  NeqAxioms.html\
  NeqDef.html\
  NeqProps.html\
  AddProps.html\
  LtProps.html\
  OppProps.html\
  SubProps.html\
  LeAxioms.html\
  LeProps.html\
  GtAxioms.html\
  GtProps.html\
  GeAxioms.html\
  GeProps.html\
  DiscrAxioms.html\
  DiscrProps.html\
  OppAxioms.html

tex: Params.tex\
  EqParams.tex\
  NSyntax.tex\
  Axioms.tex\
  EqAxioms.tex\
  NeqParams.tex\
  NeqAxioms.tex\
  NeqDef.tex\
  NeqProps.tex\
  AddProps.tex\
  LtProps.tex\
  OppProps.tex\
  SubProps.tex\
  LeAxioms.tex\
  LeProps.tex\
  GtAxioms.tex\
  GtProps.tex\
  GeAxioms.tex\
  GeProps.tex\
  DiscrAxioms.tex\
  DiscrProps.tex\
  OppAxioms.tex

gallinatex: Params.g.tex\
  EqParams.g.tex\
  NSyntax.g.tex\
  Axioms.g.tex\
  EqAxioms.g.tex\
  NeqParams.g.tex\
  NeqAxioms.g.tex\
  NeqDef.g.tex\
  NeqProps.g.tex\
  AddProps.g.tex\
  LtProps.g.tex\
  OppProps.g.tex\
  SubProps.g.tex\
  LeAxioms.g.tex\
  LeProps.g.tex\
  GtAxioms.g.tex\
  GtProps.g.tex\
  GeAxioms.g.tex\
  GeProps.g.tex\
  DiscrAxioms.g.tex\
  DiscrProps.g.tex\
  OppAxioms.g.tex

gallinahtml: Params.g.html\
  EqParams.g.html\
  NSyntax.g.html\
  Axioms.g.html\
  EqAxioms.g.html\
  NeqParams.g.html\
  NeqAxioms.g.html\
  NeqDef.g.html\
  NeqProps.g.html\
  AddProps.g.html\
  LtProps.g.html\
  OppProps.g.html\
  SubProps.g.html\
  LeAxioms.g.html\
  LeProps.g.html\
  GtAxioms.g.html\
  GtProps.g.html\
  GeAxioms.g.html\
  GeProps.g.html\
  DiscrAxioms.g.html\
  DiscrProps.g.html\
  OppAxioms.g.html

xml:: .xml_time_stamp
.xml_time_stamp: Params.vo\
  EqParams.vo\
  NSyntax.vo\
  Axioms.vo\
  EqAxioms.vo\
  NeqParams.vo\
  NeqAxioms.vo\
  NeqDef.vo\
  NeqProps.vo\
  AddProps.vo\
  LtProps.vo\
  OppProps.vo\
  SubProps.vo\
  LeAxioms.vo\
  LeProps.vo\
  GtAxioms.vo\
  GtProps.vo\
  GeAxioms.vo\
  GeProps.vo\
  DiscrAxioms.vo\
  DiscrProps.vo\
  OppAxioms.vo
	$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
	touch .xml_time_stamp

###################
#                 #
# Subdirectories. #
#                 #
###################

Leibniz:
	cd Leibniz ; $(MAKE) all

Nat:
	cd Nat ; $(MAKE) all

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

.PHONY: all opt byte archclean clean install depend xml Leibniz Nat

.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.html:
	$(COQ2HTML) $<

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

.v.g.html:
	$(GALLINA) -stdout $< | $(COQ2HTML) -f > $@

.v.g.tex:
	$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -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
	(cd Leibniz ; $(MAKE) depend)
	(cd Nat ; $(MAKE) depend)

xml::
	(cd Leibniz ; $(MAKE) xml)
	(cd Nat ; $(MAKE) xml)

install:
	@if test -z $(TARGETDIR); then echo "You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')"; exit 1; fi
	cp -f *.vo $(TARGETDIR)
	(cd Leibniz ; $(MAKE) install)
	(cd Nat ; $(MAKE) install)

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

clean:
	rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~
	(cd Leibniz ; $(MAKE) clean)
	(cd Nat ; $(MAKE) clean)

archclean:
	rm -f *.cmx *.o
	(cd Leibniz ; $(MAKE) archclean)
	(cd Nat ; $(MAKE) archclean)

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