[acl2/acl2] eaf563: Improved guard reasoning for nested stobjs (stobj-...

[GitHub]

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.

[GitHub]

Branch: refs/heads/testing