+++ /dev/null
-##############################################################################
-## 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`
-MAKE=make "COQBIN=$(COQBIN)" "OPT=$(OPT)"
-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)
-COQFLAGS=-q $(OPT) $(COQLIBS)
-COQC=$(COQBIN)coqc
-COQFULL=$(COQBIN)coqc $(FULLOPT) -q $(COQLIBS)
-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 .\
- -I $(COQTOP)/contrib/xml
-COQLIBS=-I .\
- -R . Bologna.XmlTheory\
- -I $(COQTOP)/contrib/xml
-
-###################################
-# #
-# Definition of the "all" target. #
-# #
-###################################
-
-all: XmlTheory.vo\
- iXml.cmo\
- xmltheoryentries.cmo
-
-spec: XmlTheory.vi
-
-gallina: XmlTheory.g
-
-html: XmlTheory.html
-
-tex: XmlTheory.tex
-
-gallinatex: XmlTheory.g.tex
-
-gallinahtml: XmlTheory.g.html
-
-xml: .xml_time_stamp
-.xml_time_stamp: XmlTheory.vo
- $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
- touch .xml_time_stamp
-
-####################
-# #
-# Special targets. #
-# #
-####################
-
-.PHONY: all opt byte archclean clean install depend xml
-
-.SUFFIXES: .mli .ml .cmo .cmi .cmx .v .vo .vi .g .html .tex .g.tex .g.html
-
-.mli.cmi:
- $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-.ml.cmo:
- $(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-.ml.cmx:
- $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
-
-.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
-
-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)
- cp -f *.cmo $(TARGETDIR)
-
-Makefile: Make
- mv -f Makefile Makefile.bak
- $(COQBIN)coq_makefile -f Make -o Makefile
-
-clean:
- rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~
-
-archclean:
- rm -f *.cmx *.o
-
-# WARNING
-#
-# This Makefile has been automagically generated by coq_makefile
-# Edit at your own risks !
-#
-# END OF WARNING
-