Updated :doc note-6-5 to match change about to be made to acl2-devel:

  One of the steps performed by [certify-book] has traditionally been
  to check for local incompatibilities (see [local-incompatibility])
  after admitting all the events in the book. This step involved
  rolling back the logical [world] to what it was at the start of
  certification, and then including the book (see [include-book]). As
  an optimization, we now avoid rolling back the world more than
  necessary; see [certify-book], specifically the discussion of Step
  3. Thanks to Sol Swords for requesting this optimization.

The change to system/pseudo-good-worldp.lisp supports this change.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2547 303c5b2c-9740-0410-b014-fd8f9db7be32