[Using this commit message for both acl2-books and acl2-devel:]

For oracle-apply and oracle-fncall, we no longer prohibit the
function symbol from being SYNP, MV-LIST, or RETURN-LAST; the only
illegal function symbol is IF.  Also, quoting a comment in
(defxdoc note-6-4 ...):

; Synched up the guards of oracle-apply and ev-fncall-w, and removed
; untouchables check from ev-fncall-w (since that check is now in the guard).
; This could of course allow the user to do terrible things with ev-fncall-w
; when calling it from a :program mode function, but that's not really new.  At
; least untouchables won't be allowed for ev-fncall-w at the top level or when
; using safe-mode or guard-checking :all.


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

[Using this commit message for both acl2-books and acl2-devel:]

Updated :doc note-6-4 by adding the following paragraph, to reflect a
change made in the preceding commit:

  The [table] guard on [dive-into-macros-table] has been strengthened
  in order to avoid calling untouchable functions (see
  [remove-untouchable]).


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

Improved the ACL2-Doc "i" (index) command so that if you just hit
<RETURN>, then you go to the index buffer, which now is read-only and
is in ACL2-Doc mode (so that, for example, you can hit <RETURN> while
standing on a topic in order to be taken to that topic).

Modified :DOC broken-link for the ACL2-only manual so that it gives
specific information about the source books for missing documentation
links.


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

Sorry -- here's what the preceding commit message (acl2-devel revision
1199) should have said....

ACL2-Doc browser improvements:

  Arranged to go to the BROKEN-LINK topic when using the <RETURN>
  command on a broken link [..].

  The default for the "g" command is now BROKEN-LINK when standing on
  a broken link [..].

Modified :DOC broken-link for the ACL2-only manual so that it gives
specific information about the source books for missing documentation
links.


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

Quoting :doc note-6-4:

  It had been possible to get a confusing raw Lisp error when
  submitting a [defstobj] event whose first argument is not a symbol,
  as in: (defstobj (fld :type integer :initially 0)). That user error
  is now reported gracefully by ACL2.

  When an [include-book] form is executed for a non-existent book, we
  no longer get a bogus warning about a missing compiled file. (Of
  course the compiled file is missing when the book itself is
  missing! So there's no need to report this fact.) Thanks to Caleb
  Eggensperger for bringing this issue to our attention.


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