[acl2/acl2] 96ca9c: Allow make-event expansion in a local context to s...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 96ca9cd643d3557169dbda5f4f2a6f3b437380a6
https://github.com/acl2/acl2/commit/96ca9cd643d3557169dbda5f4f2a6f3b437380a6
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2018-01-07 (Sun, 07 Jan 2018)

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

Log Message:
-----------
Allow make-event expansion in a local context to set acl2-defaults-table.

Quoting :doc note-8-1:

When performing [make-event] expansion under a surrounding [local]
context, it is no longer illegal to set the [ACL2-defaults-table]
(except of course when entering an [encapsulate] or [include-book]
within that expansion). For example, the following event formerly
caused an error but is now legal.

(local (make-event (er-progn (set-ignore-ok t)
(defun foo (x) x)
(value `(value-triple ,(length (w state)))))))


Commit: c606593f57b55a29b50ed93b7af4a72177d41e9d
https://github.com/acl2/acl2/commit/c606593f57b55a29b50ed93b7af4a72177d41e9d
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2018-01-07 (Sun, 07 Jan 2018)

Changed paths:
M doc.lisp

Log Message:
-----------
Allow make-event expansion in a local context to set acl2-defaults-table.

Quoting :doc note-8-1:

When performing [make-event] expansion under a surrounding [local]
context, it is no longer illegal to set the [ACL2-defaults-table]
(except of course when entering an [encapsulate] or [include-book]
within that expansion). For example, the following event formerly
caused an error but is now legal.

(local (make-event (er-progn (set-ignore-ok t)
(defun foo (x) x)
(value `(value-triple ,(length (w state)))))))


Compare: https://github.com/acl2/acl2/compare/1293e436a9c0...c606593f57b5

[GitHub]

Branch: refs/heads/testing

Commit: 3e08678d2b92cec1f1c20bc16ede75dd249a2561
https://github.com/acl2/acl2/commit/3e08678d2b92cec1f1c20bc16ede75dd249a2561

Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2018-01-07 (Sun, 07 Jan 2018)

Changed paths:

M axioms.lisp

Log Message:
-----------
Fixed comment typo pointed out by Alessandro Coglio.


Compare: https://github.com/acl2/acl2/compare/1293e436a9c0...3e08678d2b92