blob: 4693bd136cbccfc2d9c959c8e1ebf9cbc844c1f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
include ../config/Makefile
LOCALINCLUDES=-I ../config -I ../tools -I ../tools/coqdoc \
-I ../scripts -I ../lib -I ../kernel -I ../kernel/byterun -I ../library \
-I ../proofs -I ../tactics -I ../pretyping \
-I ../interp -I ../toplevel -I ../parsing -I ../ide/utils -I ../ide \
-I ../plugins/omega -I ../plugins/romega \
-I ../plugins/ring -I ../plugins/dp -I ../plugins/setoid_ring \
-I ../plugins/xml -I ../plugins/extraction \
-I ../plugins/fourier -I ../plugins/cc \
-I ../plugins/funind -I ../plugins/firstorder \
-I ../plugins/field -I ../plugins/subtac -I ../plugins/rtauto \
-I ../plugins/recdef
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
MLIS=$(wildcard ../lib/*.mli ../kernel/*.mli ../library/*.mli \
../pretyping/*.mli ../interp/*.mli \
../parsing/*.mli ../proofs/*.mli \
../tactics/*.mli ../toplevel/*.mli)
all:: html coq.pdf
newsyntax.dvi: newsyntax.tex
latex $<
latex $<
coq.dvi: coq.tex
latex coq
latex coq
coq.tex::
ocamldoc -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\
$(MLIS) -t "Coq mlis documentation" -intro docintro -o coq.tex
html::
ocamldoc -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\
$(MLIS) -d html -colorize-code \
-t "Coq mlis documentation" -intro docintro -css-style style.css
%.dot: ../%
ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../$*/*.ml ../$*/*.mli -o $@
%.png: %.dot
dot -Tpng $< -o $@
clean::
rm -f *~ *.log *.aux
.SUFFIXES: .tex .png
%.pdf: %.tex
pdflatex $< && pdflatex $<
|