diff options
Diffstat (limited to 'coqprime-8.4/Coqprime/Makefile.bak')
| -rw-r--r-- | coqprime-8.4/Coqprime/Makefile.bak | 203 |
1 files changed, 203 insertions, 0 deletions
diff --git a/coqprime-8.4/Coqprime/Makefile.bak b/coqprime-8.4/Coqprime/Makefile.bak new file mode 100644 index 000000000..fe49dbf29 --- /dev/null +++ b/coqprime-8.4/Coqprime/Makefile.bak @@ -0,0 +1,203 @@ +############################################################################## +## 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)/interp \ + -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \ + -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \ + -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \ + -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \ + -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \ + -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \ + -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \ + -I $(CAMLP4LIB) +ZFLAGS=$(OCAMLLIBS) $(COQSRC) +OPT= +COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) +COQC=$(COQBIN)coqc +GALLINA=gallina +COQDOC=coqdoc +CAMLC=ocamlc -c +CAMLOPTC=ocamlopt -c +CAMLLINK=ocamlc +CAMLOPTLINK=ocamlopt +COQDEP=$(COQBIN)coqdep -c +GRAMMARS=grammar.cma +CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo +PP=-pp "camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl" + +######################### +# # +# Libraries definition. # +# # +######################### + +OCAMLLIBS=-I .\ + -I ../Tactic\ + -I ../N\ + -I ../Z\ + -I ../List +COQLIBS=-I .\ + -I ../Tactic\ + -I ../N\ + -I ../Z\ + -I ../List + +################################### +# # +# Definition of the "all" target. # +# # +################################### + +VFILES=Cyclic.v\ + EGroup.v\ + Euler.v\ + FGroup.v\ + IGroup.v\ + Lagrange.v\ + LucasLehmer.v\ + Pepin.v\ + PGroup.v\ + PocklingtonCertificat.v\ + PocklingtonRefl.v\ + Pocklington.v\ + Proth.v\ + Root.v\ + Zp.v +VOFILES=$(VFILES:.v=.vo) +VIFILES=$(VFILES:.v=.vi) +GFILES=$(VFILES:.v=.g) +HTMLFILES=$(VFILES:.v=.html) +GHTMLFILES=$(VFILES:.v=.g.html) + +all: Cyclic.vo\ + EGroup.vo\ + Euler.vo\ + FGroup.vo\ + IGroup.vo\ + Lagrange.vo\ + LucasLehmer.vo\ + Pepin.vo\ + PGroup.vo\ + PocklingtonCertificat.vo\ + PocklingtonRefl.vo\ + Pocklington.vo\ + Proth.vo\ + Root.vo\ + Zp.vo + +spec: $(VIFILES) + +gallina: $(GFILES) + +html: $(HTMLFILES) + +gallinahtml: $(GHTMLFILES) + +all.ps: $(VFILES) + $(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + +all-gal.ps: $(VFILES) + $(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + + + +#################### +# # +# Special targets. # +# # +#################### + +.PHONY: all opt byte archclean clean install depend html + +.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: + $(COQDOC) -latex $< -o $@ + +.v.html: + $(COQDOC) -html $< -o $@ + +.v.g.tex: + $(COQDOC) -latex -g $< -o $@ + +.v.g.html: + $(COQDOC) -html -g $< -o $@ + +byte: + $(MAKE) all "OPT=" + +opt: + $(MAKE) all "OPT=-opt" + +include .depend + +.depend depend: + rm -f .depend + $(COQDEP) -i $(COQLIBS) $(VFILES) *.ml *.mli >.depend + $(COQDEP) $(COQLIBS) -suffix .html $(VFILES) >>.depend + +install: + mkdir -p `$(COQC) -where`/user-contrib + cp -f $(VOFILES) `$(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 $(VOFILES) $(VIFILES) $(GFILES) *~ + rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES) + +archclean: + rm -f *.cmx *.o + +html: + +# WARNING +# +# This Makefile has been automagically generated by coq_makefile +# Edit at your own risks ! +# +# END OF WARNING + |