diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-23 22:24:35 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-23 22:24:35 +0000 |
| commit | 20e9bca4d769e3d538e34469c8596e4215fd5f19 (patch) | |
| tree | 59cd2bd48577812377fe3bc32c8d068728ff9727 /Makefile.doc | |
| parent | 95dd7304f68eb155f572bf221c4d99fca85b700c (diff) | |
Fix examples in Program documentation and add comindexes for the various
commands. Update documentation of implicit arguments with the new syntax
and an explanation for the way it works in inductive type definitions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10714 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index fedde3748..3705c047a 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -86,7 +86,7 @@ doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) $(LATEX) Reference-Manual;\ $(LATEX) Reference-Manual) -doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.tex +doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex (cd doc/refman; $(PDFLATEX) Reference-Manual.tex) ### Reference Manual (browsable format) |