aboutsummaryrefslogtreecommitdiff
path: root/doc/Makefile
diff options
context:
space:
mode:
authornotin2006-03-06 15:07:54 +0000
committernotin2006-03-06 15:07:54 +0000
commitd6d5fd216c5b26cba2cb6f1d273ac3b0d9c359f8 (patch)
tree8ad3810cd65ae4b00d8a68ccae6dc8bc19a26292 /doc/Makefile
parenta997bda0383b870890c0526996319ba2d44039b4 (diff)
Deplacement du répertoire doc dans dev
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8140 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Makefile')
-rw-r--r--doc/Makefile67
1 files changed, 0 insertions, 67 deletions
diff --git a/doc/Makefile b/doc/Makefile
deleted file mode 100644
index a0bef8976c..0000000000
--- a/doc/Makefile
+++ /dev/null
@@ -1,67 +0,0 @@
-
-# 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 $@
-