diff -r ac93579530ea -r b009afd1ace5 doc-src/Logics/CTT.tex
--- a/doc-src/Logics/CTT.tex	Tue Aug 03 13:05:13 1999 +0200
+++ b/doc-src/Logics/CTT.tex	Tue Aug 03 13:05:54 1999 +0200
@@ -2,6 +2,8 @@
 \chapter{Constructive Type Theory}
 \index{Constructive Type Theory|(}
 
+\underscoreoff %this file contains _ in rule names
+
 Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
 be viewed at many different levels.  It is a formal system that embodies
 the principles of intuitionistic mathematics; it embodies the