[acl2/acl2] d149ca: Misc. defun-sk improvement include support for dec...

[GitHub]

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

Changed paths:
M books/centaur/lispfloat/ops-exec.lisp
M books/system/doc/acl2-doc.lisp
M books/workshops/2000/manolios/pipeline/pipeline/top/defun-weak-sk.lisp
M doc.lisp
M other-events.lisp

Log Message:
-----------
Misc. defun-sk improvement include support for declare form and improved guard verification. Modified a book that was failing to certify with 32-bit CCL.

Quoting :doc note-7-3 (here, omitting the first two bulleted items as
indicated, since they were essentially in the :doc already).

The following improvements have been made to [defun-sk]. See
[defun-sk] for detailed documentation.

[...]

* Defun-sk now accepts [declare] forms immediately after the formal
parameters, as is the case for [defun]. Thanks to Eric Smith
for suggesting this enhancement. The :witness-dcls keyword is
still supported as well, but may become deprecated in the
future.
* An issue involving [guard] verification for defun-sk forms has been
addressed. Thanks to Alessandro Coglio for suggesting this
improvement.
* Syntax checking now produces improved error messages for defun-sk.

Modified books/centaur/lispfloat/ops-exec.lisp to accommodate a
failure in 32-bit CCL. Thanks to Waqar Ahmad and Jared Davis for
helpful emails.

[GitHub]

Branch: refs/heads/testing