Branch: refs/heads/master
Home:
https://github.com/acl2/acl2
Commit: eaf563d232fd62cab3c1f59615dedae3ccd737fa
https://github.com/acl2/acl2/commit/eaf563d232fd62cab3c1f59615dedae3ccd737fa
Author: Matt Kaufmann <
matthew.j...@gmail.com>
Date: 2017-04-19 (Wed, 19 Apr 2017)
Changed paths:
M basis-a.lisp
M books/add-ons/hash-stobjs.lisp
M books/misc/check-acl2-exports.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M other-events.lisp
M translate.lisp
Log Message:
-----------
Improved guard reasoning for nested stobjs (stobj-let). Added utility checkpoint-summary-limit. Improved an error message and a :doc URL.
Quoting :doc note-7-4:
A small change in [defstobj] can lead to improved automation for some
[guard] proofs involving [stobj-let]. Thanks to Sol Swords for
sending an example (included in a Lisp comment in (deflabel
note-7-4 ...)).
Added utility checkpoint-summary-limit. Thanks to Mihir Mehta for an
email leading to this addition.
; Improved an error message when stobj-let references a stobj not declared by
; :stobjs, thanks to a bug report and example from Sol Swords.
Also, improved reference to double-rewrite paper in :doc
double-rewrite, thanks to feedback from Mihir Mehta.