diff --git a/scripts/extract-comments.py b/scripts/extract-comments.py
index 2b4f854f326fbb2d97a36e1e761597e2edb6cb39..21d396e67b41599219f9ddf96a64f7a12dda6b48 100755
--- a/scripts/extract-comments.py
+++ b/scripts/extract-comments.py
@@ -6,6 +6,7 @@ import os
 import re
 
 INLINE_CODE_RE = re.compile(r'\[[^]]*?\]')
+VERBATIM_RE = re.compile(r'<<.*?>>')
 
 def comment_ranges(src):
     "Identify comments in Coq .v files."
@@ -41,8 +42,10 @@ def process(opts, fname):
     out = sys.stdout
     for (a, b) in comment_ranges(src):
         txt = src[a:b]
-        print(INLINE_CODE_RE.sub('', txt))
-#     out.close()
+        txt = txt.replace('\n', ' ')
+        txt = VERBATIM_RE.sub('', txt)
+        txt = INLINE_CODE_RE.sub('', txt)
+        print(txt)
 
 def parse_args():
     parser = argparse.ArgumentParser(
diff --git a/scripts/flag-typos-in-comments.sh b/scripts/flag-typos-in-comments.sh
index 07ecd96b3ac561f8738f16e7564c0daf109b4d48..72d3d9a808dfc9e6b2bf796d7bf3f84da90936e9 100755
--- a/scripts/flag-typos-in-comments.sh
+++ b/scripts/flag-typos-in-comments.sh
@@ -10,7 +10,6 @@ do
 
 	#Here, sed is used to remove verbatim text (enclosed in <<>>)
 	for WORD in $(scripts/extract-comments.py "$SRC" \
-		| sed 's/<<.*>>//g' \
 		| hunspell -p $KNOWN_EXCEPTIONS -l -d en_US \
 		| sort \
 		| uniq)