diff options
| author | herbelin | 2007-05-16 18:30:02 +0000 |
|---|---|---|
| committer | herbelin | 2007-05-16 18:30:02 +0000 |
| commit | 3101ff981d36359f74d5996447ba70f41398e72b (patch) | |
| tree | 20efdde892be0d74eee3e69470cfcca99763ac2b /doc | |
| parent | 407f120d4b6a8d829cbf8efdfe5796444dda5a73 (diff) | |
- MAJ entêtes des fichiers produits par coq_makefile
- Correction de bugs dans la reconnaissance d'un "*)" potentiel dans
les lignes correspondant au mécanisme "section" de coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9826 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/coqdoc.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index 63594a18f9..0e3cab3e61 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -104,7 +104,7 @@ combinations, e.g. \paragraph{Sections.} Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the -line). One star is a section, two stars a sub-section, etc. +line) followed by a space. One star is a section, two stars a sub-section, etc. The section title is given on the remaining of the line. Example: \begin{verbatim} @@ -152,7 +152,7 @@ escape sequences: \paragraph{Verbatim.} Verbatim material is introduced by a leading \verb+<<+ and closed by -\verb+>>+. Example: +\verb+>>+ at the beginning of a line. Example: \begin{verbatim} Here is the corresponding caml code: << |