[acl2/acl2] 305508: Fixed proof-builder bug in rewrite (i.e., r) comma...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 305508ef4bf56d905f4f9864200c5ec71e610848
https://github.com/acl2/acl2/commit/305508ef4bf56d905f4f9864200c5ec71e610848
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2017-10-18 (Wed, 18 Oct 2017)

Changed paths:
M books/system/doc/acl2-doc.lisp
M other-events.lisp

Log Message:
-----------
Fixed proof-builder bug in rewrite (i.e., r) command. Tweaked in :doc free-variables and some :doc about guards in signatures.

Quoting :doc note-7-5:

A bug in the [proof-builder]'s command, rewrite (or equivalently, r;
see [ACL2-pc::rewrite], avoided creating necessary subgoals, which
can presumably be unsound. That bad behavior could occur when the
third (and optional) argument of that command was a non-nil value
other than t.

Thanks to Eric Smith for email queries leading to the :doc
improvements.


Commit: 1611f65f451ffb6837b76f578d7e0529aec4d314
https://github.com/acl2/acl2/commit/1611f65f451ffb6837b76f578d7e0529aec4d314
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2017-10-18 (Wed, 18 Oct 2017)

Changed paths:
M doc.lisp

Log Message:
-----------
Synched doc.lisp


Compare: https://github.com/acl2/acl2/compare/ef8ef1e716a6...1611f65f451f

[GitHub]

Branch: refs/heads/testing