"make source-doc" builds documentation of mli in html and pdf at

dev/ocamldoc/

old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)

"make clean" cleans dev/ocamldoc/ properly

wierd? calls of dependency graph generation leave unchanged

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 8 insertions, 62 deletions

diff --git a/dev/Makefile b/dev/Makefile
deleted file mode 100644
index 4693bd136..000000000
--- a/dev/Makefile
+++ /dev/null
@@ -1,53 +0,0 @@
-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 $<
\ No newline at end of file
diff --git a/dev/docintro b/dev/ocamldoc/docintro
index 3d37d5374..3c0e262d4 100644
--- a/dev/docintro
+++ b/dev/ocamldoc/docintro
@@ -1,10 +1,9 @@
 {!indexlist}
 
-This is Coq, a proof assistant for the Calculus of Inductive Construction.
+This is Coq, a proof assistant for the Calculus of Inductive Constructions.
 This document describes the implementation of Coq.
 It has been automatically generated from the source of
-Coq using ocamldoc, a literate programming tool for
-Objective Caml  freely available at http://caml.inria.fr/.
+Coq using {{:http://caml.inria.fr/}ocamldoc}.
 The source files are organized in several directories ordered like that:
 
 {ol {- Utility libraries : lib
@@ -13,8 +12,8 @@ describes the various utility libraries used in the code
 of Coq.}
 {- Kernel : kernel
 
-describes the \Coq\ kernel, which is a type checker for the Calculus
-of Inductive Construction.}
+describes the Coq kernel, which is a type checker for the Calculus
+of Inductive Constructions.}
 {- Library : library
 
 describes the Coq library, which is made of two parts:
@@ -30,11 +29,11 @@ describes the Coq library, which is made of two parts:
 {- Front abstract syntax of terms : interp
 
 describes the translation from Coq context-dependent
-front abstract syntax of terms {v front v} to and from the
+front abstract syntax of terms {v constr_expr v} to and from the
 context-free, untyped, raw form of constructions {v rawconstr v}.}
 {- Parsers and printers : parsing
 
-describes the implementation of the \Coq\ parsers and printers.}
+describes the implementation of the Coq parsers and printers.}
 {- Proof engine : proofs
 
 describes the Coq proof engine, which is also called
diff --git a/dev/html/style.css b/dev/ocamldoc/html/style.css
index b8f02a15f..c2c45b629 100644
--- a/dev/html/style.css
+++ b/dev/ocamldoc/html/style.css
@@ -23,11 +23,11 @@ a:active {
 }

 

 .superscript {

-  font-size: 4 

+  font-size: 8 

 }

 

 .subscript {

-  font-size: 4 

+  font-size: 8 

 }

 

 .comment {