[acl2/acl2] 6c9469: Added :conjunct and :substitute keywords to print-...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 6c94693dbdfe3d8389fb709f936b635f668eea6b
https://github.com/acl2/acl2/commit/6c94693dbdfe3d8389fb709f936b635f668eea6b
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2015-11-18 (Wed, 18 Nov 2015)

Changed paths:
M axioms.lisp
M books/misc/bash-bsd.lisp
M books/misc/bash.lisp
M books/misc/simp.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/removable-runes.lisp
M doc.lisp
M other-events.lisp

Log Message:
-----------
Added :conjunct and :substitute keywords to print-gv, and added utility to set defaults, set-print-gv-defaults. Untranslated all print-gv output. Changed :doc topic name ERROR-TRIPLES to ERROR-TRIPLE. Synched doc.lisp.

Quoting :doc note-7-2:

The utility [print-gv] now takes additional keyword arguments,
:conjunct and :substitute, which respectively show a specific
conjunct of the [guard] evaluation that produced nil, and avoid
[flet] in favor of substituting actuals (even at the risk of
duplication). See [print-gv], and see [set-print-gv-defaults] for a
utility that sets default values for the keyword arguments. Thanks
to Eric Smith for requesting these enhancements and for helpful
discussions. Note that the system default value for the
:evisc-tuple keyword is now the value of the form
(print-gv-evisc-tuple).

See [set-print-gv-defaults] for a new utility for setting default
values for the keyword arguments of [print-gv]. Thanks to Eric
Smith for requesting this feature and for helpful discussions.

Also quoting :doc note-7-2 -- this item was already there, except that
the part about untranslate is new, fixed in this commit.

[Guard] violation error messages printed 'ACL2_INVISIBLE::|The Live
State Itself| where they should have printed STATE; similarly for
the utility [print-gv], which also failed to print entirely in
user-level ``untranslated'' syntax. These problems have been fixed.
Thanks to Eric Smith for bringing the ``STATE'' bug to our
attention.

Changed :doc topic name ERROR-TRIPLES to ERROR-TRIPLE, and fixed and
added links correspondingly.

Also synched doc.lisp.

[GitHub]

Branch: refs/heads/testing