Added new value :ignore-certs for include-book keyword :uncertified-okp.

Quoting :doc note-7-0:

  A new value for [include-book] keyword argument :uncertified-okp is
  :ignore-certs, which specifies that all certificate files are to be
  ignored during inclusion of this book and all of its sub-books. See
  [include-book]. Thanks to Sol Swords for requesting this feature.

Changed the message about "Reading .port file" to an Observation, so
that it can be turned off.

Improved an include-book error message by distinguishing the case of
being under certify-book.
Merge
Minor doc updates and synched doc.lisp.