diff --git a/bin/man/autcross.x b/bin/man/autcross.x
index 4158aca11..bda9a9cce 100644
--- a/bin/man/autcross.x
+++ b/bin/man/autcross.x
@@ -59,29 +59,29 @@ Information about how the execution of the tool went.
 values:
 .RS
 .TP
-\f(CW"ok"\fR
+\fC"ok"\fR
 The tool ran succesfully (this does not imply that the produced
 automaton is correct) and autcross could parse the resulting
 automaton.  In this case \fBexit_code\fR is always 0.
 .TP
-\f(CW"timeout"\fR
+\fC"timeout"\fR
 The tool ran for more than the number of seconds
 specified with the \fB\-\-timeout\fR option.  In this
 case \fBexit_code\fR is always -1.
 .TP
-\f(CW"exit code"\fR
+\fC"exit code"\fR
 The tool terminated with a non-zero exit code.
 \fBexit_code\fR contains that value.
 .TP
-\f(CW"signal"\fR
+\fC"signal"\fR
 The tool terminated with a signal.
 \fBexit_code\fR contains that signal's number.
 .TP
-\f(CW"parse error"\fR
+\fC"parse error"\fR
 The tool terminated normally, but autcross could not
 parse its output.  In this case \fBexit_code\fR is always -1.
 .TP
-\f(CW"no output"\fR
+\fC"no output"\fR
 The tool terminated normally, but without creating the specified
 output file.  In this case \fBexit_code\fR is always -1.
 .RE
diff --git a/bin/man/ltl2tgba.x b/bin/man/ltl2tgba.x
index b34aa02ab..bb41aed73 100644
--- a/bin/man/ltl2tgba.x
+++ b/bin/man/ltl2tgba.x
@@ -13,7 +13,7 @@ condition, meanings that a run of the automaton is accepted iff it
 visits ininitely often multiple acceptance sets, and it also uses
 transition-based acceptance, i.e., those acceptance sets are sets of
 transitions.  TGBA are often more consise than traditional Büchi
-automata.  For instance the LTL formula \f(CWGFa & GFb\fR can be
+automata.  For instance the LTL formula \fCGFa & GFb\fR can be
 translated into a single-state TGBA while a traditional Büchi
 automaton would need 3 states.  Compare
 .PP
@@ -158,11 +158,11 @@ are not recognized, i.e., infinite words that start with a bad prefix.
 .PP
 Because of this limited expressiveness, a monitor for some given LTL
 or PSL formula may accept a larger language than the one specified by
-the formula.  For instance a monitor for the LTL formula \f(CWa U b\fR
-will reject (for instance) any word starting with \f(CW!a&!b\fR as
+the formula.  For instance a monitor for the LTL formula \fCa U b\fR
+will reject (for instance) any word starting with \fC!a&!b\fR as
 there is no way such a word can validate the formula, but it will not
-reject a finite prefix repeating only \f(CWa&!b\fR as such a prefix
-could be extented in a way that is comptible with \f(CWa U b\fR.
+reject a finite prefix repeating only \fCa&!b\fR as such a prefix
+could be extented in a way that is comptible with \fCa U b\fR.
 .PP
 For more information about monitors, we refer the readers to the
 following two papers (the first paper describes the construction of
diff --git a/bin/man/ltlcross.x b/bin/man/ltlcross.x
index f16b17a74..c16adb3ed 100644
--- a/bin/man/ltlcross.x
+++ b/bin/man/ltlcross.x
@@ -12,7 +12,7 @@ for 100 random formulas, using a timeout of 2 minutes.  Because
 knows those tools, there is no need to specify their input and
 output. A trace of the execution of the two tools, including any
 potential issue detected, is reported on standard error, while
-statistics are written to \f(CWresults.json\fR.
+statistics are written to \fCresults.json\fR.
 .PP
 .in +4n
 .nf
@@ -26,14 +26,14 @@ The next command compares
 .BR ltl3ba ,
 and
 .BR ltl2tgba (1)
-on a set of formulas saved in file \f(CWinput.ltl\fR.
+on a set of formulas saved in file \fCinput.ltl\fR.
 Statistics are again writen
-as CSV into \f(CWresults.csv\fR.  This examples specify the
+as CSV into \fCresults.csv\fR.  This examples specify the
 input and output for each tool, to show how this can be done.
-Note the use of \f(CW%L\fR to indicate that the formula passed t
+Note the use of \fC%L\fR to indicate that the formula passed t
 for the formula in
 .BR spin (1)'s
-format, and \f(CW%f\fR for the
+format, and \fC%f\fR for the
 formula in Spot's format.  Each of these tool produces an
 automaton in a different format (respectively, LBTT's format,
 Spin's never claims, and HOA format), but Spot's parser can
@@ -51,7 +51,7 @@ distinguish and understand these three formats.
 Rabin or Streett automata output by
 .B ltl2dstar
 in its historical format can be read from a
-file specified with \f(CW%D\fR instead of \f(CW%O\fR.  For instance:
+file specified with \fC%D\fR instead of \fC%O\fR.  For instance:
 .PP
 .in +4n
 .nf
@@ -99,7 +99,7 @@ The formula translated.
 \fBtool\fR
 The tool used to translate this formula.  This is either the value of the
 full \fICOMMANDFMT\fR string specified on the command-line, or,
-if \fICOMMANDFMT\fR has the form \f(CW{\fISHORTNAME\fR\f(CW}\fR\fICMD\fR,
+if \fICOMMANDFMT\fR has the form \fC{\fISHORTNAME\fR\fC}\fR\fICMD\fR,
 the value of \fISHORTNAME\fR.
 .TP
 \fBexit_status\fR, \fBexit_code\fR
@@ -110,29 +110,29 @@ Otherwise, \fBexit_status\fR is a string that can take the following
 values:
 .RS
 .TP
-\f(CW"ok"\fR
+\fC"ok"\fR
 The translator ran succesfully (this does not imply that the produced
 automaton is correct) and ltlcross could parse the resulting
 automaton.  In this case \fBexit_code\fR is always 0.
 .TP
-\f(CW"timeout"\fR
+\fC"timeout"\fR
 The translator ran for more than the number of seconds
 specified with the \fB\-\-timeout\fR option.  In this
 case \fBexit_code\fR is always -1.
 .TP
-\f(CW"exit code"\fR
+\fC"exit code"\fR
 The translator terminated with a non-zero exit code.
 \fBexit_code\fR contains that value.
 .TP
-\f(CW"signal"\fR
+\fC"signal"\fR
 The translator terminated with a signal.
 \fBexit_code\fR contains that signal's number.
 .TP
-\f(CW"parse error"\fR
+\fC"parse error"\fR
 The translator terminated normally, but ltlcross could not
 parse its output.  In this case \fBexit_code\fR is always -1.
 .TP
-\f(CW"no output"\fR
+\fC"no output"\fR
 The translator terminated normally, but without creating the specified
 output file.  In this case \fBexit_code\fR is always -1.
 .RE
@@ -150,7 +150,7 @@ translated automaton.  Column \fBedges\fR counts the number of edges
 (labeled by Boolean formulas) in the automaton seen as a graph, while
 \fBtransitions\fR counts the number of assignment-labeled transitions
 that might have been merged into a formula-labeled edge.  For instance
-an edge labeled by \f(CWtrue\fR will be counted as 2^3=8 transitions if
+an edge labeled by \fCtrue\fR will be counted as 2^3=8 transitions if
 the automaton uses 3 atomic propositions.
 .TP
 \fBscc\fR, \fBnonacc_scc\fR, \fBterminal_scc\fR, \fBweak_scc\fR, \fBstrong_scc\fR
diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x
index 6aa4a385e..25a1a89ff 100644
--- a/bin/man/spot-x.x
+++ b/bin/man/spot-x.x
@@ -10,7 +10,7 @@ spot-x \- Common fine-tuning options and environment variables.
 .\" Add any additional description here
 
 [SAT\-MINIMIZE VALUES]
-When the sat-minimize=K option is used to enable SAT-based
+When the \fBsat-minimize=K\fR option is used to enable SAT-based
 minimization of deterministic automata, a SAT solver is
 used to minimize an input automaton with N states into an
 output automaton with 1≤M≤N states.  The parameter K specifies
@@ -72,12 +72,12 @@ passed to the printer by suffixing the output format with
 .in +4n
 .EX
 % SPOT_DEFAULT_FORMAT=dot=bar autfilt ...
-.EN
+.EE
 .in -4n
 is the same as running
 .in +4n
 .EX
-% autfilt --dot=bar ...
+% autfilt \-\-dot=bar ...
 .EE
 .in -4n
 but the use of the environment variable makes more sense if you set
@@ -92,9 +92,9 @@ executed in debug mode, showing how the input is processed.
 \fBSPOT_DOTDEFAULT\fR
 Whenever the \fB\-\-dot\fR option is used without argument (even
 implicitely via \fBSPOT_DEFAULT_FORMAT\fR), the contents of this
-variable is used as default argument.  If you have some default
+variable are used as default argument.  If you have some default
 settings in \fBSPOT_DOTDEFAULT\fR and want to append to options
-\f(CWxyz\fR temporarily for one call, use \fB\-\-dot=.xyz\fR:
+\fCxyz\fR temporarily for one call, use \fB\-\-dot=.xyz\fR:
 the dot character will be replaced by the contents of the
 \fBSPOT_DOTDEFAULT\fR environment variable.
 
@@ -123,7 +123,7 @@ is actually used)
 .TP
 \fBSPOT_O_CHECK\fR
 Specifies the default algorithm that should be used
-by the \f(CWis_obligation()\fR function.  The value should
+by the \fCis_obligation()\fR function.  The value should
 be one of the following:
 .RS
 .RS
@@ -141,24 +141,24 @@ by a weak and deterministic Büchi automata.
 
 .TP
 \fBSPOT_OOM_ABORT\fR
-If this variable is set, Out-Of-Memory errors will \f(CWabort()\fR the
+If this variable is set, Out-Of-Memory errors will \fCabort()\fR the
 program (potentially generating a coredump) instead of raising an
 exception.  This is useful to debug a program and to obtain a stack
 trace pointing to the function doing the allocation.  When this
-variable is unset (the default), \f(CWstd::bad_alloc\fR are thrown on
+variable is unset (the default), \fCstd::bad_alloc\fR are thrown on
 memory allocation failures, and the stack is usually unwinded up to
 top-level, losing the original context of the error.  Note that at
-least \f(CWltlcross\fR has some custom handling of
-\f(CWstd::bad_alloc\fR to recover from products that are too large (by
+least \fCltlcross\fR has some custom handling of
+\fCstd::bad_alloc\fR to recover from products that are too large (by
 ignoring them), and setting this variable will interfer with that.
 
 .TP
 \fBSPOT_PR_CHECK\fR
 Select the default algorithm that must be used to check the persistence
 or recurrence property of a formula f. The values it can take are between
-1 and 3. All  methods work either on f or !f thanks to the duality of
+1 and 3. All methods work either on f or !f thanks to the duality of
 persistence and recurrence classes.  See
-.UR https://spot.lrde.epita.fr/hierarchy.html
+.UR https://spot.lre.epita.fr/hierarchy.html
 this page
 .UE
 for more details. If it is set to:
@@ -196,8 +196,8 @@ format.
 If set, this variable should indicate how to call an external
 SAT\-solver \- by default, Spot uses PicoSAT, which is distributed
 with. This is used by the sat\-minimize option described above.
-The format to follow is the following: \f(CW"<sat_solver> [options] %I >%O"\fR.
-The escape sequences \f(CW%I\fR and \f(CW%O\fR respectively
+The format to follow is the following: \fC"<sat_solver> [options] %I >%O"\fR.
+The escape sequences \fC%I\fR and \fC%O\fR respectively
 denote the names of the input and output files.  These temporary files
 are created in the directory specified by \fBSPOT_TMPDIR\fR or
 \fBTMPDIR\fR (see below). The SAT\-solver should follow the convention
@@ -281,7 +281,7 @@ This is mostly useful for debugging.
 .TP
 \fBSPOT_XCNF\fR
 Assign a folder path to this variable to generate XCNF files whenever
-SAT\-based minimization is used \- the file is outputed as "incr.xcnf"
+SAT\-based minimization is used \- the file is output as "incr.xcnf"
 in the specified directory. This feature works only with an external
 SAT\-solver. See \fBSPOT_SATSOLVER\fR to know how to provide one. Also note
 that this needs an incremental approach without restarting the encoding i.e
@@ -290,8 +290,8 @@ autfilt (see sat\-minimize options described above or autfilt man page).
 The XCNF format is the one used by the SAT incremental competition.
 
 [BIBLIOGRAPHY]
-
-The following papers are related to some of the options and environment variables.
+The following papers are related to some of the options and
+environment variables.
 
 .TP
 1.
@@ -344,7 +344,7 @@ Kyveli Doveri and Pierre Ganty and Nicolas Mazzocchi:
 FORQ-Based Language Inclusion Formal Testing.
 Proceedings of CAV'22. LNCS 13372.
 
-The containment check implemented as spot::contains_forq(), and
+The containment check implemented as \fCspot::contains_forq()\fR, and
 used for Büchi automata when \fBSPOT_CONTAINMENT_CHECK=forq\fR.
 
 [SEE ALSO]
diff --git a/bin/man/spot.x b/bin/man/spot.x
index eaa1e933b..037069d39 100644
--- a/bin/man/spot.x
+++ b/bin/man/spot.x
@@ -27,6 +27,6 @@ that are listed below.
 .BR randltl (1)
 .BR spot-x (7)
 
-.UR https://spot.lrde.epita.fr/
+.UR https://spot.lre.epita.fr/
 The Spot web page.
 .UE