Merge PR #19058: Fix the man pages' formatting.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

man/coq-tex.1

@@ -1,10 +1,10 @@
-.TH COQ-TEX 1
-
+.TH COQ\-TEX 1
+.
 .SH NAME
-coq-tex \- Process Coq phrases embedded in LaTeX files
-
+coq\-tex \- process Coq phrases embedded in LaTeX files
+.
 .SH SYNOPSIS
-.B coq-tex
+.B coq\-tex
 [
 .BI \-o \ output-file
 ]
@@ -29,97 +29,105 @@ coq-tex \- Process Coq phrases embedded in LaTeX files
 [
 .B \-small
 ]
-.I input-file ...
-
-
+.I input-file .\|.\|.
+.
+.
 .SH DESCRIPTION
-
+.
 The
-.B coq-tex
+.B coq\-tex
 filter extracts Coq phrases embedded in LaTeX files, evaluates
 them, and insert the outcome of the evaluation after each phrase.
-
+.PP
 Three LaTeX environments are provided to include Coq code in
 the input files:
 .TP
 .B coq_example
 The phrases between \\begin{coq_example} and \\end{coq_example} are
-evaluated and copied into the output file. Each phrase is followed by
-the response of the toplevel loop.
+evaluated and copied into the output file.
+Each phrase is followed by the response of the toplevel loop.
 .TP
 .B coq_example*
 The phrases between \\begin{coq_example*} and \\end{coq_example*} are
-evaluated and copied into the output file. The responses of the
-toplevel loop are discarded.
+evaluated and copied into the output file.
+The responses of the toplevel loop are discarded.
 .TP
 .B coq_eval
 The phrases between \\begin{coq_eval} and \\end{coq_eval} are
-silently evaluated. They are not copied into the output file, and the
-responses of the toplevel loop are discarded.
+silently evaluated.
+They are not copied into the output file, and the responses of the
+toplevel loop are discarded.
 .PP
 The resulting LaTeX code is stored in the file
 .IR file \&.v.tex
 if the input file has a name of the form
 .IR file \&.tex,
 otherwise the name of the output file is the name of the input file
 with `.v.tex' appended.
-
+.PP
 The files produced by
-.B coq-tex
+.B coq\-tex
 can be directly processed by LaTeX.
 Both the Coq phrases and the toplevel output are typeset in
 typewriter font.
-
+.
 .SH OPTIONS
-
+.
 .TP
 .BI \-o \ output-file
-Specify the name of a file where the LaTeX output is to be stored. A
-dash `\-' causes the LaTeX output to be printed on standard output.
+Specify the name of a file where the LaTeX output is to be stored.
+A dash `\-' causes the LaTeX output to be printed on standard output.
 .TP
 .BI \-n \ line-width
-Set the line width. The default is 72 characters. The responses of the
-toplevel loop are folded if they are longer than the line width. No
-folding is performed on the Coq input text.
+Set the line width.
+The default is 72 characters.
+The responses of the toplevel loop are folded if they are longer than
+the line width.
+No folding is performed on the Coq input text.
 .TP
 .BI \-image \ coq-image
 Cause the file
-.IR coq-image
-to be executed to evaluate the Coq phrases. By default,
-this is the command
-.IR coqtop
+.I coq-image
+to be executed to evaluate the Coq phrases.
+By default, this is the command
+.I coqtop
 without specifying any path which is used to evaluate the Coq phrases.
 .TP
 .B \-w
 Cause lines to be folded on a space character whenever possible,
-avoiding word cuts in the output. By default, folding occurs at
-the line width, regardless of word cuts.
+avoiding word cuts in the output.
+By default, folding occurs at the line width, regardless of word cuts.
 .TP
 .B \-v
-Verbose mode. Prints the Coq answers on the standard output.
+Verbose mode.
+Prints the Coq answers on the standard output.
 Useful to detect errors in Coq phrases.
 .TP
 .B \-sl
-Slanted mode. The Coq answers are written in a slanted font.
+Slanted mode.
+The Coq answers are written in a slanted font.
 .TP
 .B \-hrule
-Horizontal lines mode. The Coq parts are written between two
-horizontal lines.
+Horizontal lines mode.
+The Coq parts are written between two horizontal lines.
 .TP
 .B \-small
-Small font mode. The Coq parts are written in a smaller font.
-
-
+Small font mode.
+The Coq parts are written in a smaller font.
+.
+.
 .SH CAVEATS
-The \\begin... and \\end... phrases must sit on a line by themselves,
-with no characters before the backslash or after the closing brace.
+The \\begin.\|.\|. and \\end.\|.\|. phrases must sit on a line by
+themselves, with no characters before the backslash or after the closing
+brace.
 Each Coq phrase must be terminated by `.' at the end of a line.
 Blank space is accepted between `.' and the newline, but any other
-character will cause coq-tex to ignore the end of the phrase,
-resulting in an incorrect shuffling of the responses into the phrases.
+character will cause
+.B coq\-tex
+to ignore the end of the phrase, resulting in an incorrect shuffling of
+the responses into the phrases.
 (The responses ``lag behind''.)
-
+.
 .SH SEE ALSO
-
-.B coqtop
-(1).
+.
+.BR coqtop (1)

man/coq_makefile.1

@@ -1,33 +1,35 @@
-.TH COQ 1
-
+.\" TODO: actually document this thing
+.TH COQ_MAKEFILE 1
+.
 .SH NAME
-coq_makefile \- The Coq Proof Assistant makefile generator
-
-
+coq_makefile \- generate makefiles for Coq proof development
+.
+.
 .SH SYNOPSIS
 .B coq_makefile
 [
-.B arguments
+.I arguments
 ]
-
+.
 .SH DESCRIPTION
-
+.
 .B coq_makefile
 is a makefile generator for Coq proof developments.
-
+.
 .SH OPTIONS
-
+.
 .TP
-.BI \-h
-Will give you a description of the whole list of options of coq_makefile.
-
+.B \-h
+Will give you a description of the whole list of options of
+.BR coq_makefile .
+.
 .SH SEE ALSO
-
+.
 .BR coqtop (1),
 .BR coqtc (1),
-.BR coqdep (1).
-.br
+.BR coqdep (1)
+.PP
 .I
 The Coq Reference Manual.
-.I
+.PP
 The Coq web site: http://coq.inria.fr

man/coqc.1

@@ -1,64 +1,66 @@
-.TH COQ 1
-
+.TH COQC 1
+.
 .SH NAME
-coqc \- The Coq Proof Assistant compiler
-
-
+coqc \- Coq compiler
+.
+.
 .SH SYNOPSIS
 .B coqc
 [
-.B general \ Coq \ options
+general Coq options
 ]
 .I file
-
-
+.
+.
 .SH DESCRIPTION
-
+.
 .B coqc
 is the batch compiler for the Coq Proof Assistant.
-The options are basically the same as coqtop(1).
-.IR file.v \&
+The options are basically the same as
+.BR coqtop (1).
+.I file.v
 is the vernacular file to compile.
-.IR file \&
+.I file
 must be formed
-only with the characters `a` to  `Z`, `0`-`9` or `_` and must begin
+only with the characters `a' to `Z', `0' to `9' or `_' and must begin
 with a letter.
 The compiler produces an object file
 .IR file.vo \&.
-
+.PP
 For interactive use of Coq, see
-.BR coqtop(1).
-
-
+.BR coqtop (1).
+.
+.
 .SH OPTIONS
-
+.
+.\" TODO: Coqc is not a script.  Correct this claim.
 .B coqc
 is a script that simply runs
 .B coqtop
 with option
-.B \-compile
-it accepts the same options as
-.B coqtop.
-
+.BR \-compile .
+It accepts the same options as
+.BR coqtop .
+.
 .TP
 .BI \-image \ bin
-use
+Use
 .I bin
 as underlying
 .B coqtop
 instead of the default one.
-
+.
 .TP
-.BI \-verbose
-print the compiled file on the standard output.
-
+.B \-verbose
+Print the compiled file on the standard output.
+.
 .SH SEE ALSO
-
+.
 .BR coqtop (1),
 .BR coq_makefile (1),
-.BR coqdep (1).
-.br
+.BR coqdep (1)
+.PP
 .I
 The Coq Reference Manual.
-.I
+.PP
 The Coq web site: http://coq.inria.fr