Merge PR #12293: Fix timestamp of coqchk manpage

Reviewed-by: Zimmi48

man/coq-tex.1

@@ -1,4 +1,4 @@
-.TH COQ-TEX 1 "29 March 1995"
+.TH COQ-TEX 1
 
 .SH NAME
 coq-tex \- Process Coq phrases embedded in LaTeX files
@@ -66,7 +66,7 @@ with `.v.tex' appended.
 
 The files produced by
 .B coq-tex
-can be directly processed by LaTeX. 
+can be directly processed by LaTeX.
 Both the Coq phrases and the toplevel output are typeset in
 typewriter font.
 
@@ -86,7 +86,7 @@ folding is performed on the Coq input text.
 Cause the file
 .IR coq-image
 to be executed to evaluate the Coq phrases. By default,
-this is the command 
+this is the command
 .IR coqtop
 without specifying any path which is used to evaluate the Coq phrases.
 .TP

man/coq_makefile.1

@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1
 
 .SH NAME
 coq_makefile \- The Coq Proof Assistant makefile generator

man/coqc.1

@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1
 
 .SH NAME
 coqc \- The Coq Proof Assistant compiler
@@ -19,14 +19,14 @@ is the batch compiler for the Coq Proof Assistant.
 The options are basically the same as coqtop(1).
 .IR file.v \&
 is the vernacular file to compile.
-.IR file \& 
+.IR file \&
 must be formed
 only with the characters `a` to  `Z`, `0`-`9` or `_` and must begin
 with a letter.
 The compiler produces an object file
 .IR file.vo \&.
 
-For interactive use of Coq, see 
+For interactive use of Coq, see
 .BR coqtop(1).
 
 
@@ -35,7 +35,7 @@ For interactive use of Coq, see
 .B coqc
 is a script that simply runs
 .B coqtop
-with option 
+with option
 .B \-compile
 it accepts the same options as
 .B coqtop.

man/coqchk.1

@@ -1,4 +1,4 @@
-.TH COQ 1 "July 7, 201"
+.TH COQ 1
 
 .SH NAME
 coqchk \- The Coq Proof Checker compiled libraries verifier
@@ -29,7 +29,7 @@ short or qualified logical name, or by their filename.
 
 .TP
 .BI \-I \ dir, \ \-\-include \ dir
-add directory 
+add directory
 .I dir
 in the include path
 

man/coqdep.1

@@ -1,4 +1,4 @@
-.TH COQ 1 "28 March 1995" "Coq tools"
+.TH COQ 1
 
 .SH NAME
 coqdep \- Compute inter-module dependencies for Coq and Caml programs
@@ -31,13 +31,13 @@ When a directory is given as argument, it is recursively looked at.
 Dependencies of Coq modules are computed by looking at
 .IR Require \&
 commands (Require, Require Export, Require Import),
-.IR Declare \& 
-.IR ML \& 
+.IR Declare \&
+.IR ML \&
 .IR Module \&
 commands and
 .IR Load \&
 commands. Dependencies relative to modules from the Coq library are not
-printed except if 
+printed except if
 .BR \-boot \&
 is given.
 
@@ -51,27 +51,27 @@ directives and the dot notation
 .TP
 .BI \-f \ file
 Read filenames and options -I, -R and -Q from a _CoqProject FILE.
-.TP 
+.TP
 .BI \-I/\-Q/\-R \ options
 Have the same effects on load path and modules names as for other
 coq commands (coqtop, coqc).
-.TP 
+.TP
 .BI \-coqlib \ directory
 Indicates where is the Coq library. The default value has been
 determined at installation time, and therefore this option should not
 be used under normal circumstances.
-.TP 
+.TP
 .BI \-exclude-dir \ dir
 Skips subdirectory
 .IR dir \ during
 .BR -R/-Q \ search.
-.TP 
+.TP
 .B \-sort
 Output the given file name ordered by dependencies.
 .TP
 .B \-vos
 Output dependencies for .vos files (this is not the default as it breaks dune's Coq mode)
-.TP 
+.TP
 .B \-boot
 For coq developers, prints dependencies over coq library files
 (omitted by default).
@@ -106,7 +106,7 @@ Consider the files (in the same directory):
 
 where
 .TP
-.BI \+ 
+.BI \+
 D.ml contains the commands `open A', `open B' and `type t = C.t' ;
 .TP
 .BI \+

man/coqdoc.1

@@ -1,4 +1,4 @@
-.TH coqdoc 1 "April, 2006"
+.TH coqdoc 1
 
 .SH NAME
 coqdoc \- A documentation tool for the Coq proof assistant
@@ -47,12 +47,12 @@ Select a TeXmacs output.
 Redirect the output to stdout
 .TP
 .BI \-o \ file, \-\-output \ file
-Redirect the output into the file 
+Redirect the output into the file
 .I file.
 .TP
 .BI \-d \ dir, \ \-\-directory \ dir
-Output files into directory 
-.I dir 
+Output files into directory
+.I dir
 instead of current directory (option
 \-d does not change the filename specified with option \-o, if any).
 .TP
@@ -102,7 +102,7 @@ Generate one page for each category and each letter in the index,
 together with a top page index.html.
 
 .SS Table of contents option
- 
+
 .TP
 .B \-toc, \ \-\-table\-of\-contents
 Insert a table of contents. For a LATEX output, it inserts a
@@ -136,7 +136,7 @@ Set the base path where the Coq files are installed, especially style files coqd
 .BI \-R \ dir \  coqdir
 Map physical directory dir to Coq logical directory coqdir (similarly
 to Coq option \-R).
-.B Note: 
+.B Note:
 option \-R only has effect on the files following it on the command
 line, so you will probably need to put this option first.
 
@@ -155,26 +155,26 @@ Light mode. Suppress proofs (as with \-g) and the following commands:
         * Require
         * Transparent / Opaque
         * Implicit Argument / Implicits
-        * Section / Variable / Hypothesis / End 
+        * Section / Variable / Hypothesis / End
 
 The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
 
 .SS Language options
- 
+
 Default behavior is to assume ASCII 7 bits input files.
 
-.TP 
+.TP
 .B \-latin1, \ \-\-latin1
 Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1
 \-\-charset iso\-8859\-1.
 
-.TP 
+.TP
 .B \-utf8, \ \-\-utf8
 Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc
 utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at
 http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/.
 
-.TP 
+.TP
 .BI \-\-inputenc \ string
 Give a LATEX input encoding, as an option to LATEX package inputenc.
 
@@ -187,4 +187,3 @@ Specify the HTML character set, to be inserted in the HTML header.
 
 .I
 The Coq Reference Manual from http://coq.inria.fr/
-

man/coqide.1

@@ -1,4 +1,4 @@
-.TH COQIDE 1 "July 16, 2004"
+.TH COQIDE 1
 
 .SH NAME
 coqide \- The Coq Proof Assistant graphical interface
@@ -17,7 +17,7 @@ is a gtk graphical interface for the Coq proof assistant.
 
 For command-line-oriented use of Coq, see
 .BR coqtop (1)
-; for batch-oriented use of Coq, see 
+; for batch-oriented use of Coq, see
 .BR coqc (1).
 
 

man/coqtop.1

@@ -1,4 +1,4 @@
-.TH COQ 1 "October 11, 2006"
+.TH COQ 1
 
 .SH NAME
 coqtop \- The Coq Proof Assistant toplevel system
@@ -17,7 +17,7 @@ is the toplevel system of Coq, for interactive use.
 It reads phrases on the standard input, and prints results on the
 standard output.
 
-For batch-oriented use of Coq, see 
+For batch-oriented use of Coq, see
 .BR coqc(1).
 
 
@@ -29,12 +29,12 @@ Help. Will give you the complete list of options accepted by coqtop.
 
 .TP
 .BI \-I \ dir, \ \-\-include \ dir
-add directory 
+add directory
 .I dir
 in the include path
 
 .TP
-.BI \-R \ dir\ coqdir          
+.BI \-R \ dir\ coqdir
 recursively map physical
 .I dir
 to logical
@@ -67,7 +67,7 @@ load Coq file
 (Load filename.)
 
 .TP
-.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename 
+.BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename
 load verbosely Coq file
 .I filename.v
 (Load Verbose filename.)

man/coqtop.byte.1

@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1
 
 .SH NAME
 coqtop.byte \- The bytecode Coq toplevel
@@ -31,5 +31,3 @@ and
 The Coq Reference Manual.
 .I
 The Coq web site: http://coq.inria.fr
-
-

man/coqtop.opt.1

@@ -1,4 +1,4 @@
-.TH COQ 1 "April 25, 2001"
+.TH COQ 1
 
 .SH NAME
 coqtop.opt \- The native-code Coq toplevel
@@ -31,5 +31,3 @@ and
 The Coq Reference Manual.
 .I
 The Coq web site: http://coq.inria.fr
-
-

man/coqwc.1

@@ -1,4 +1,4 @@
-.TH COQ 1 "16 March 2004" "Coq tools"
+.TH COQ 1
 
 .SH NAME
 coqwc \- print the number of specification, proof and comment lines in