summaryrefslogtreecommitdiff
path: root/dev/doc/Makefile
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /dev/doc/Makefile
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'dev/doc/Makefile')
-rw-r--r--dev/doc/Makefile67
1 files changed, 67 insertions, 0 deletions
diff --git a/dev/doc/Makefile b/dev/doc/Makefile
new file mode 100644
index 00000000..a0bef897
--- /dev/null
+++ b/dev/doc/Makefile
@@ -0,0 +1,67 @@
+
+# Makefile for doc/
+
+all:: newparse
+#newsyntax.dvi minicoq.dvi
+
+
+OBJS=lex.cmo ast.cmo parse.cmo syntax.cmo
+
+newparse: $(OBJS) syntax.mli lex.ml syntax.ml
+ ocamlc -o newparse $(OBJS)
+
+.ml.cmo:
+ ocamlc -c $<
+
+.mli.cmi:
+ ocamlc -c $<
+
+.mll.ml:
+ ocamllex $<
+
+.mly.ml:
+ ocamlyacc -v $<
+
+.mly.mli:
+ ocamlyacc -v $<
+
+clean::
+ rm -f *.cm* *.output syntax.ml syntax.mli lex.ml newparse
+
+parse.cmo: ast.cmo
+syntax.cmi: parse.cmo
+syntax.cmo: lex.cmo parse.cmo syntax.cmi
+lex.cmo: syntax.cmi
+ast.cmo: ast.ml
+
+newsyntax.dvi: newsyntax.tex
+ latex $<
+ latex $<
+
+coq.dvi: coq.tex
+ latex coq
+ latex coq
+
+coq.tex::
+ make -C .. doc/coq.tex
+
+depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \
+ proofs.dep.ps tactics.dep.ps toplevel.dep.ps interp.dep.ps
+
+%.dot: ../%
+ (cd ../$*; ocamldep *.ml *.mli) | ocamldot -lr > $@
+
+%.dep.ps: %.dot
+ dot -Tps $< -o $@
+
+clean::
+ rm -f *~ *.log *.aux
+
+.SUFFIXES: .tex .dvi .ps .cmo .cmi .mli .ml .mll .mly
+
+.tex.dvi:
+ latex $< && latex $<
+
+.dvi.ps:
+ dvips $< -o $@
+