diff -r 7fca5aabcbb0 -r 839ab9c054f6 doc-src/ERRATA.txt
--- a/doc-src/ERRATA.txt	Wed May 10 08:38:52 1995 +0200
+++ b/doc-src/ERRATA.txt	Thu May 11 10:33:07 1995 +0200
@@ -27,6 +27,7 @@
 Introduction
 
 page 67: show_brackets is another flag, controlling display of bracketting
+show_sorts:=true forces display of types
 
 Tactics