Added comments about issues with user stobj and state as formals of the same function, which calls trans-eval.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1276 5d84a466-a78b-0930-a311-59b22171a541
Quoting :doc note-6-5:

  We fixed a soundness bug for nested [stobj]s (see [stobj-let]). In
  the case of a stobj producer variable that is not a child stobj, it
  had been possible to update that stobj without returning it. Thanks
  to Sol Swords for reporting this bug and providing a corresponding
  proof of nil, which is included in a comment in the form (defxdoc
  note-6-5 ...) in [community-books] file
  books/system/doc/acl2-doc.lisp.)


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1277 5d84a466-a78b-0930-a311-59b22171a541