--- /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`
+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
+COQWEB=coqweb
+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. #
+# #
+###################################
+
+VFILES=st_base.v\
+ st_logic.v\
+ st_nat.v\
+ st_arith.v\
+ Standard.v\
+ xt_fin.v\
+ tbs_base.v\
+ tbs_rel.v\
+ tbs_op.v\
+ tbs_rop.v\
+ tbs_fun.v\
+ tbs_fin.v\
+ Toolbox.v
+VOFILES=$(VFILES:.v=.vo)
+VIFILES=$(VFILES:.v=.vi)
+GFILES=$(VFILES:.v=.g)
+HTMLFILES=$(VFILES:.v=.html)
+GHTMLFILES=$(VFILES:.v=.g.html)
+
+all: st_base.vo\
+ st_logic.vo\
+ st_nat.vo\
+ st_arith.vo\
+ Standard.vo\
+ xt_fin.vo\
+ tbs_base.vo\
+ tbs_rel.vo\
+ tbs_op.vo\
+ tbs_rop.vo\
+ tbs_fun.vo\
+ tbs_fin.vo\
+ Toolbox.vo
+
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(HTMLFILES)
+
+gallinahtml: $(GHTMLFILES)
+
+all.ps: $(VFILES)
+ $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.ps: $(GFILES)
+ $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`
+
+xml:: .xml_time_stamp
+.xml_time_stamp: st_base.vo\
+ st_logic.vo\
+ st_nat.vo\
+ st_arith.vo\
+ Standard.vo\
+ xt_fin.vo\
+ tbs_base.vo\
+ tbs_rel.vo\
+ tbs_op.vo\
+ tbs_rop.vo\
+ tbs_fun.vo\
+ tbs_fin.vo\
+ Toolbox.vo
+ $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
+ touch .xml_time_stamp
+
+####################
+# #
+# Special targets. #
+# #
+####################
+
+.PHONY: all opt byte archclean clean install depend xml
+
+.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:
+ $(COQWEB) $< -o $@
+
+.v.html:
+ $(COQWEB) -html $< -o $@
+
+.g.g.tex:
+ $(COQWEB) $< -o $@
+
+.g.g.html:
+ $(COQWEB) -html $< -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
+
+xml::
+
+install:
+ mkdir -p `$(COQC) -where`/user-contrib
+ cp -f *.vo `$(COQC) -where`/user-contrib
+
+Makefile: Make
+ mv -f Makefile Makefile.bak
+ $(COQBIN)coq_makefile -f Make -o Makefile
+
+clean:
+ rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~
+ rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
+
+archclean:
+ rm -f *.cmx *.o
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+