Imported Upstream version 0.2.pl2upstream/0.2.pl2

1 files changed, 319 insertions, 0 deletions

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..a56d4b6
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,319 @@
+#############################################################################
+##  v      #                   The Coq Proof Assistant                     ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
+##   \VV/  #                                                               ##
+##    //   #  Makefile automagically generated by coq_makefile V8.3        ##
+#############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -R . AAC_tactics -opt MLIFILES = $(MLFILES:.ml=.mli) AAC_coq.ml AAC_helper.ml AAC_search_monad.ml AAC_matcher.ml AAC_theory.ml AAC_print.ml AAC_rewrite.ml AAC.v Instances.v Tutorial.v Caveats.v -f magic.txt 
+#
+
+# 
+# This Makefile may take 3 arguments passed as environment variables:
+#   - COQBIN to specify the directory where Coq binaries resides;
+#   - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.
+COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
+CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')"
+ifndef CAMLP4BIN
+  CAMLP4BIN:=$(CAMLBIN)
+endif
+
+CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)
+
+##########################
+#                        #
+# Libraries definitions. #
+#                        #
+##########################
+
+OCAMLLIBS:=
+COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \
+  -I $(COQLIB)/library -I $(COQLIB)/parsing \
+  -I $(COQLIB)/pretyping -I $(COQLIB)/interp \
+  -I $(COQLIB)/proofs -I $(COQLIB)/tactics \
+  -I $(COQLIB)/toplevel \
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+COQLIBS:= -R . AAC_tactics
+COQDOCLIBS:=-R . AAC_tactics
+
+##########################
+#                        #
+# Variables definitions. #
+#                        #
+##########################
+
+ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
+OPT:=
+COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+ifdef CAMLBIN
+  COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)
+endif
+COQC:=$(COQBIN)coqc
+COQDEP:=$(COQBIN)coqdep -c
+GALLINA:=$(COQBIN)gallina
+COQDOC:=$(COQBIN)coqdoc
+COQMKTOP:=$(COQBIN)coqmktop
+CAMLLIB:=$(shell $(CAMLBIN)ocamlc -where)
+CAMLC:=$(CAMLBIN)ocamlc -c -rectypes
+CAMLOPTC:=$(CAMLBIN)ocamlopt -c -rectypes
+CAMLLINK:=$(CAMLBIN)ocamlc -rectypes
+CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes
+GRAMMARS:=grammar.cma
+CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
+CAMLP4OPTIONS:=
+MLIFILES=$(MLFILES:.ml=.mli)
+PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
+
+###################################
+#                                 #
+# Definition of the "all" target. #
+#                                 #
+###################################
+
+VFILES:=AAC.v\
+  Instances.v\
+  Tutorial.v\
+  Caveats.v
+VOFILES:=$(VFILES:.v=.vo)
+GLOBFILES:=$(VFILES:.v=.glob)
+VIFILES:=$(VFILES:.v=.vi)
+GFILES:=$(VFILES:.v=.g)
+HTMLFILES:=$(VFILES:.v=.html)
+GHTMLFILES:=$(VFILES:.v=.g.html)
+MLFILES:=AAC_coq.ml\
+  AAC_helper.ml\
+  AAC_search_monad.ml\
+  AAC_matcher.ml\
+  AAC_theory.ml\
+  AAC_print.ml\
+  AAC_rewrite.ml
+CMOFILES:=$(MLFILES:.ml=.cmo)
+CMIFILES:=$(MLFILES:.ml=.cmi)
+CMXFILES:=$(MLFILES:.ml=.cmx)
+CMXSFILES:=$(MLFILES:.ml=.cmxs)
+OFILES:=$(MLFILES:.ml=.o)
+
+all: $(VOFILES) $(CMOFILES) $(CMXSFILES) doc\
+  aac_tactics.cmxs\
+  aac_tactics.cmxa\
+  aac_tactics.cma\
+  .depend
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)
+
+gallinahtml: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)
+
+all.ps: $(VFILES)
+	$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.ps: $(VFILES)
+	$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all.pdf: $(VFILES)
+	$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.pdf: $(VFILES)
+	$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+
+
+###################
+#                 #
+# Custom targets. #
+#                 #
+###################
+
+doc: $(MLIFILES)
+	mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc
+
+aac_tactics.cmxs: $(CMXFILES)
+	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)
+
+aac_tactics.cmxa: $(CMXFILES)
+	$(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES)
+
+aac_tactics.cma: $(CMOFILES)
+	$(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)
+
+.depend: $(MLIFILES)
+	$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend
+
+####################
+#                  #
+# Special targets. #
+#                  #
+####################
+
+.PHONY: all opt byte archclean clean install depend html
+
+%.cmi: %.mli
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+
+%.cmo: %.ml
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<
+
+%.cmx: %.ml
+	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<
+
+%.cmxs: %.ml
+	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<
+
+%.cmo: %.ml4
+	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+
+%.cmx: %.ml4
+	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+
+%.cmxs: %.ml4
+	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<
+
+%.ml.d: %.ml
+	$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $(PP) "$<" > "$@"
+
+%.vo %.glob: %.v
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+%.vi: %.v
+	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+%.g: %.v
+	$(GALLINA) $<
+
+%.tex: %.v
+	$(COQDOC) -latex $< -o $@
+
+%.html: %.v %.glob
+	$(COQDOC) -html $< -o $@
+
+%.g.tex: %.v
+	$(COQDOC) -latex -g $< -o $@
+
+%.g.html: %.v %.glob
+	$(COQDOC) -html -g $< -o $@
+
+%.v.d: %.v
+	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+byte:
+	$(MAKE) all "OPT:=-byte"
+
+opt:
+	$(MAKE) all "OPT:=-opt"
+
+install:
+	mkdir -p $(COQLIB)/user-contrib
+	(for i in $(VOFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
+	 done)
+	(for i in $(CMOFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
+	 done)
+	(for i in $(CMIFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
+	 done)
+	(for i in $(CMXSFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/AAC_tactics/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/AAC_tactics/$$i; \
+	 done)
+
+clean:
+	rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~
+	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
+	rm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)
+	- rm -rf html
+	- rm -rf doc
+	- rm -f aac_tactics.cmxs
+	- rm -f aac_tactics.cmxa
+	- rm -f aac_tactics.cma
+	- rm -f .depend
+
+archclean:
+	rm -f *.cmx *.o
+
+
+printenv: 
+	@echo CAMLC =	$(CAMLC)
+	@echo CAMLOPTC =	$(CAMLOPTC)
+	@echo CAMLP4LIB =	$(CAMLP4LIB)
+
+.dummy: magic.txt
+	mv -f Makefile Makefile.bak
+	$(COQBIN)coq_makefile -f magic.txt -o Makefile
+
+
+-include $(VFILES:.v=.v.d)
+.SECONDARY: $(VFILES:.v=.v.d)
+
+-include $(MLFILES:.ml=.ml.d)
+.SECONDARY: $(MLFILES:.ml=.ml.d)
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+
+
+# override inadequate coq_makefile auto-regeneration
+Makefile: make_makefile magic.txt files.txt
+	./make_makefile
+
+# We want to keep the proofs in Caveats and the Tutorial
+world: $(VOFILES) doc
+	- mkdir -p html
+	$(COQDOC) -toc -utf8 -html -g $(COQDOCLIBS) -d html $(VFILES)
+	$(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Tutorial.v
+	$(COQDOC) --no-index --no-externals -s -utf8 -html $(COQDOCLIBS) -d html Caveats.v
+
+# additional dependencies for AAC (since aac_tactics.cmxs/cma are not
+# around the first time we run make, coqdep issues a warning and
+# ignores this dependency)
+# (one can safely select one of theses dependencies according to 
+#  coq' compilation mode--bytecode or native)
+AAC.vo: aac_tactics.cmxa aac_tactics.cmxs aac_tactics.cma
+
+# .depend contains dependencies for .mli files
+-include .depend
+.SECONDARY: .depend
+