[acl2/acl2] b9b118: Allow non-formals in defstub output signature. Al...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: b9b118f7fa2fcad59e4341d726f8b2f4fae9e7fd
https://github.com/acl2/acl2/commit/b9b118f7fa2fcad59e4341d726f8b2f4fae9e7fd
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-08-25 (Thu, 25 Aug 2016)

Changed paths:
M basis-a.lisp
M basis-b.lisp
M books/interface/emacs/acl2-interface.el
M books/system/doc/acl2-doc.lisp
M doc.lisp

Log Message:
-----------
Allow non-formals in defstub output signature. Allow non-numeric argument for exit commands. Fixed menu's monitor command. Fixed a couple of small :doc bugs.

Quoting :doc note-7-3:

It is no longer illegal for [defstub] to use an old style output
signature with variables that are not among the formals. For
example, the following is now legal (note that u is not among the
list (x y) of formal parameters): (defstub foo (x y) (mv u x)).
Thanks to Eric Smith for pointing out that this behavior is allowed
by the documentation (specifically, see the discussion of
``Old Style'' in the documentation for [signature]).

The macro [good-bye] no longer requires its argument to be a
(natural) number. Any argument is now valid, and as before, is
evaluated; if that argument is not an integer, it is treated as 0.
The same change applies to the aliases for [good-bye], namely
[exit] and [quit]. Thanks to Eric Smith for suggesting this change.

Quoting a comment in (defxdoc note-7-3 ...):

; The defstub macro now calls a new function defstub-fn to generate the
; macroexpansion.

Fixed bug in (rarely used?) menu stuff, to avoid assuming that a rule
to be monitored is a :definition rule. Thanks to Eric Smith for
bringing this bug to my attention.

Documentation tweaks following suggestions from Eric Smith:

- Clarified defined-constant (:doc system-utilities).
- Removed a duplicate line from :doc defstub.

[GitHub]

Branch: refs/heads/testing