X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2FMakefile;fp=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2FMakefile;h=b3936376b3b42e8d1a66de06d22ef7c73dff5808;hb=1b21075e987872a2e3103203b4e67c939e4a9f6a;hp=0000000000000000000000000000000000000000;hpb=ea6b99ed26a954a578e3c88909479dcf9cab7345;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/Makefile b/helm/coq-contribs/LAMBDA-TYPES/Makefile
new file mode 100644
index 000000000..b3936376b
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/Makefile
@@ -0,0 +1,352 @@
+##############################################################################
+##                 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\
+  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\
+  drop_defs.v\
+  drop_props.v\
+  csubst0_defs.v\
+  csubst1_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\
+  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\
+  cpr0_defs.v\
+  cpr0_props.v\
+  pc1_defs.v\
+  pc3_defs.v\
+  pc3_props.v\
+  pc3_gen.v\
+  pc3_subst0.v\
+  pc3_gen_context.v\
+  ty0_defs.v\
+  ty0_lift.v\
+  ty0_props.v\
+  ty0_subst0.v\
+  ty0_gen_context.v\
+  csub0_defs.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\
+  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\
+  drop_defs.vo\
+  drop_props.vo\
+  csubst0_defs.vo\
+  csubst1_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\
+  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\
+  cpr0_defs.vo\
+  cpr0_props.vo\
+  pc1_defs.vo\
+  pc3_defs.vo\
+  pc3_props.vo\
+  pc3_gen.vo\
+  pc3_subst0.vo\
+  pc3_gen_context.vo\
+  ty0_defs.vo\
+  ty0_lift.vo\
+  ty0_props.vo\
+  ty0_subst0.vo\
+  ty0_gen_context.vo\
+  csub0_defs.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\
+  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\
+  drop_defs.vo\
+  drop_props.vo\
+  csubst0_defs.vo\
+  csubst1_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\
+  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\
+  cpr0_defs.vo\
+  cpr0_props.vo\
+  pc1_defs.vo\
+  pc3_defs.vo\
+  pc3_props.vo\
+  pc3_gen.vo\
+  pc3_subst0.vo\
+  pc3_gen_context.vo\
+  ty0_defs.vo\
+  ty0_lift.vo\
+  ty0_props.vo\
+  ty0_subst0.vo\
+  ty0_gen_context.vo\
+  csub0_defs.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
+