Update the manual.

doc/manual/compiler.texinfo

@@ -723,8 +723,7 @@ variable in the loop body.
 Ideally, the compiler would consider @emph{all} type declarations to
 be assertions, so that adding type declarations to a program, no
 matter how incorrect they might be, would @emph{never} cause undefined
-behavior. However, the compiler is known to fall short of this goal in
-two areas:
+behavior. However, the compiler is known to fall short of this goal:
 
 @itemize
 
@@ -734,37 +733,7 @@ function are supposed to be checked by the function. If the function
 type is proclaimed before function definition, type checks are
 inserted by the compiler, but the standard allows the reversed order,
 in which case the compiler will trust the declaration.
-
-@item
-The compiler cannot check types of an unknown number of values; if the
-number of generated values is unknown, but the number of consumed is
-known, only consumed values are checked.
-
-For example,
-
-@lisp
-(defun foo (x)
-  (the integer (bar x)))
-@end lisp
-
-causes the following compiler diagnostic to be emitted:
-
-@example
-; note: type assertion too complex to check:
-;  (VALUES INTEGER &REST T).
-@end example
-
-A partial workaround is instead write:
-
-@lisp
-(defun foo (x)
-  (the (values integer &optional) (bar x)))
-@end lisp
-
-@end itemize
-
-These are important issues, but are not necessarily easy to fix, so
-they may, alas, remain in the system for a while.
+@code{(optimize (debug 3))} will not trust any FTYPE declarations.
 
 @node Compiler Policy
 @comment  node-name,  next,  previous,  up