[acl2/acl2] 84222b: Fixed bugs in tracking and disabling compound-reco...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 84222b2b85b4b53771b564e74ed9d8be0a197729
https://github.com/acl2/acl2/commit/84222b2b85b4b53771b564e74ed9d8be0a197729
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2017-01-08 (Sun, 08 Jan 2017)

Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M other-events.lisp
M rewrite.lisp
M simplify.lisp
M type-set-b.lisp

Log Message:
-----------
Fixed bugs in tracking and disabling compound-recognizer rules. Added full :doc for untranslate. Moved existing items on acl2-doc to the right section.

Quoting :doc note-7-4:

Fixed bugs in the tracking and disabling of [compound-recognizer]
rules. Thanks to Dmitry Nadezhin for pointing out this bug, indeed,
sending an example and analyzing it to point to system function
term-and-typ-to-lookup, which was indeed the one that had the bug.

Replaced the defpointer for untranslate with a proper xdoc topic.
Thanks to Eric Smith for bringing to our attention this deficiency.

Two items on acl2-doc had been in the section on "Changes at the
System Level", but are now in the more suitable section, "EMACS
Support".

[GitHub]

Branch: refs/heads/testing