[PATCH 6/7] future/formalregress: Use \co{} for spin

formalregress.tex is using \co{} for spin in most cases.  Use it always
for better consistency.

Signed-off-by: SeongJae Park <[email protected]>
---
 future/formalregress.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/future/formalregress.tex b/future/formalregress.tex
index a50df4ad..b1a39b29 100644
--- a/future/formalregress.tex
+++ b/future/formalregress.tex
@@ -155,7 +155,7 @@ testing, which is in fact the topic of this section.
 It is critically important that formal-verification tools correctly
 model their environment.
 One all-too-common omission is the memory model, where a great
-many formal-verification tools, including Promela/spin, are
+many formal-verification tools, including Promela/\co{spin}, are
 restricted to \IXh{sequential}{consistency}.
 The QRCU experience related in
 \cref{sec:formal:Is QRCU Really Correct?}
@@ -359,7 +359,7 @@ What is needed is a tool that gives at least \emph{some} information
 as to where the bug is located and the nature of that bug.
 
 The \co{cbmc} output includes a traceback mapping back to the source
-code, similar to Promela/spin's, as does Nidhugg.
+code, similar to Promela/\co{spin}'s, as does Nidhugg.
 Of course, these tracebacks can be quite long, and analyzing them
 can be quite tedious.
 However, doing so is usually quite a bit faster
-- 
2.17.1