diff options
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/coqdoc.sty | 2 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 9de9a38ff9..f49f9f0066 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -1,5 +1,5 @@ -% This is coqdoc.sty, by Jean-Christophe Filliâtre +% This is coqdoc.sty, by Jean-Christophe Filliâtre % This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc) % % You can modify the following macros to customize the appearance diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 88a102d85c..f67ab5f95a 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -450,7 +450,7 @@ let gen_mult_files l = if (!header_trailer) then Output.trailer (); close_out_file() end - (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) + (* NB: for latex and texmacs, a separated toc or index is meaningless... *) let read_glob_file vfile f = try Index.read_glob vfile f |