+++ /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=base_tactics.v\
- base_hints.v\
- base_types.v\
- base_blt.v\
- base_rewrite.v\
- Base.v\
- terms_defs.v\
- tlt_defs.v\
- contexts_defs.v\
- lift_defs.v\
- lift_gen.v\
- lift_props.v\
- lift_tlt.v\
- drop_defs.v\
- drop_props.v\
- subst0_defs.v\
- subst0_gen.v\
- subst0_lift.v\
- subst0_subst0.v\
- subst0_confluence.v\
- subst0_tlt.v\
- subst1_defs.v\
- subst1_gen.v\
- subst1_lift.v\
- subst1_subst1.v\
- subst1_confluence.v\
- csubst0_defs.v\
- csubst1_defs.v\
- fsubst0_defs.v\
- pr0_defs.v\
- pr0_lift.v\
- pr0_gen.v\
- pr0_subst0.v\
- pr0_confluence.v\
- pr0_subst1.v\
- pr1_defs.v\
- pr1_confluence.v\
- cpr0_defs.v\
- pr2_defs.v\
- pr2_lift.v\
- pr2_gen.v\
- pr2_confluence.v\
- pr2_subst1.v\
- pr2_gen_context.v\
- pr3_defs.v\
- pr3_props.v\
- pr3_gen.v\
- pr3_confluence.v\
- pr3_subst1.v\
- pr3_gen_context.v\
- pc1_defs.v\
- pc1_props.v\
- pc3_defs.v\
- pc3_props.v\
- pc3_gen.v\
- pc3_subst0.v\
- pc3_gen_context.v\
- ty0_defs.v\
- ty0_gen.v\
- ty0_lift.v\
- ty0_props.v\
- ty0_subst0.v\
- ty0_gen_context.v\
- csub0_defs.v\
- csub0_props.v\
- ty0_sred.v\
- ty0_sred_props.v\
- LambdaDelta.v
-VOFILES=$(VFILES:.v=.vo)
-VIFILES=$(VFILES:.v=.vi)
-GFILES=$(VFILES:.v=.g)
-HTMLFILES=$(VFILES:.v=.html)
-GHTMLFILES=$(VFILES:.v=.g.html)
-
-all: base_tactics.vo\
- base_hints.vo\
- base_types.vo\
- base_blt.vo\
- base_rewrite.vo\
- Base.vo\
- terms_defs.vo\
- tlt_defs.vo\
- contexts_defs.vo\
- lift_defs.vo\
- lift_gen.vo\
- lift_props.vo\
- lift_tlt.vo\
- drop_defs.vo\
- drop_props.vo\
- subst0_defs.vo\
- subst0_gen.vo\
- subst0_lift.vo\
- subst0_subst0.vo\
- subst0_confluence.vo\
- subst0_tlt.vo\
- subst1_defs.vo\
- subst1_gen.vo\
- subst1_lift.vo\
- subst1_subst1.vo\
- subst1_confluence.vo\
- csubst0_defs.vo\
- csubst1_defs.vo\
- fsubst0_defs.vo\
- pr0_defs.vo\
- pr0_lift.vo\
- pr0_gen.vo\
- pr0_subst0.vo\
- pr0_confluence.vo\
- pr0_subst1.vo\
- pr1_defs.vo\
- pr1_confluence.vo\
- cpr0_defs.vo\
- pr2_defs.vo\
- pr2_lift.vo\
- pr2_gen.vo\
- pr2_confluence.vo\
- pr2_subst1.vo\
- pr2_gen_context.vo\
- pr3_defs.vo\
- pr3_props.vo\
- pr3_gen.vo\
- pr3_confluence.vo\
- pr3_subst1.vo\
- pr3_gen_context.vo\
- pc1_defs.vo\
- pc1_props.vo\
- pc3_defs.vo\
- pc3_props.vo\
- pc3_gen.vo\
- pc3_subst0.vo\
- pc3_gen_context.vo\
- ty0_defs.vo\
- ty0_gen.vo\
- ty0_lift.vo\
- ty0_props.vo\
- ty0_subst0.vo\
- ty0_gen_context.vo\
- csub0_defs.vo\
- csub0_props.vo\
- ty0_sred.vo\
- ty0_sred_props.vo\
- LambdaDelta.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: base_tactics.vo\
- base_hints.vo\
- base_types.vo\
- base_blt.vo\
- base_rewrite.vo\
- Base.vo\
- terms_defs.vo\
- tlt_defs.vo\
- contexts_defs.vo\
- lift_defs.vo\
- lift_gen.vo\
- lift_props.vo\
- lift_tlt.vo\
- drop_defs.vo\
- drop_props.vo\
- subst0_defs.vo\
- subst0_gen.vo\
- subst0_lift.vo\
- subst0_subst0.vo\
- subst0_confluence.vo\
- subst0_tlt.vo\
- subst1_defs.vo\
- subst1_gen.vo\
- subst1_lift.vo\
- subst1_subst1.vo\
- subst1_confluence.vo\
- csubst0_defs.vo\
- csubst1_defs.vo\
- fsubst0_defs.vo\
- pr0_defs.vo\
- pr0_lift.vo\
- pr0_gen.vo\
- pr0_subst0.vo\
- pr0_confluence.vo\
- pr0_subst1.vo\
- pr1_defs.vo\
- pr1_confluence.vo\
- cpr0_defs.vo\
- pr2_defs.vo\
- pr2_lift.vo\
- pr2_gen.vo\
- pr2_confluence.vo\
- pr2_subst1.vo\
- pr2_gen_context.vo\
- pr3_defs.vo\
- pr3_props.vo\
- pr3_gen.vo\
- pr3_confluence.vo\
- pr3_subst1.vo\
- pr3_gen_context.vo\
- pc1_defs.vo\
- pc1_props.vo\
- pc3_defs.vo\
- pc3_props.vo\
- pc3_gen.vo\
- pc3_subst0.vo\
- pc3_gen_context.vo\
- ty0_defs.vo\
- ty0_gen.vo\
- ty0_lift.vo\
- ty0_props.vo\
- ty0_subst0.vo\
- ty0_gen_context.vo\
- csub0_defs.vo\
- csub0_props.vo\
- ty0_sred.vo\
- ty0_sred_props.vo\
- LambdaDelta.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
-
projects / helm.git / blobdiff