[acl2/acl2] c22bcf: Documentation fixes:

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: c22bcf311812e31af8ececa734ca5ef709fcf145
https://github.com/acl2/acl2/commit/c22bcf311812e31af8ececa734ca5ef709fcf145
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-12-01 (Thu, 01 Dec 2016)

Changed paths:
M books/centaur/aignet/aignet-absstobj.lisp
M books/centaur/bitops/limited-shifts.lisp
M books/centaur/fty/docgen.lisp
M books/centaur/sv/svex/a4vec-ops.lisp
M books/centaur/sv/svex/aig-arith.lisp
M books/centaur/sv/svex/select.lisp
M books/centaur/vl/mlib/arithclass.lisp
M books/centaur/vl/mlib/selfsize.lisp
M books/centaur/vl/server/describe.lisp
M books/centaur/vl/transforms/addnames.lisp
M books/std/util/defalist-base.lisp
M books/std/util/deflist-base.lisp
M books/std/util/defmapappend.lisp
M books/xdoc/base.lisp
M books/xdoc/top.lisp

Log Message:
-----------
Documentation fixes:
- Add a defxdoc option :no-override and a corresponding defsection
option :no-xdoc-override, meaning that if the topic exists at the time
of the table event -- not the make-event expansion -- then it is not
overridden. Used this in some documentation-generating macros like
deflist to avoid overwriting the documentation for ACL2 built-in
functions like integer-listp.
- Fixed various other documentation problems in vl, sv, fty, etc.

[GitHub]

Branch: refs/heads/master

Commit: d2b2cf482564f71a4f2f9c853c02220570b2c800
https://github.com/acl2/acl2/commit/d2b2cf482564f71a4f2f9c853c02220570b2c800
Author: David L. Rager <rag...@gmail.com>

Date: 2016-12-01 (Thu, 01 Dec 2016)

Changed paths:

A books/projects/sat/lrat/lrat-checker.lisp
A books/projects/sat/lrat/lrat-parser.lisp
A books/projects/sat/lrat/sat-drat-claim-1.lisp
A books/projects/sat/lrat/sat-drat-claim-2-3.lisp
A books/projects/sat/lrat/sat-drat-claim-2.lisp
A books/projects/sat/lrat/satisfiable-add-proof-clause-base.lisp
A books/projects/sat/lrat/satisfiable-add-proof-clause-drat.lisp
A books/projects/sat/lrat/satisfiable-add-proof-clause-rup.lisp
A books/projects/sat/lrat/satisfiable-add-proof-clause.lisp
A books/projects/sat/lrat/satisfiable-maybe-shrink-formula.lisp
A books/projects/sat/lrat/soundness.lisp
A books/projects/sat/lrat/tests/LICENSE
A books/projects/sat/lrat/tests/README
A books/projects/sat/lrat/tests/driver.lisp
A books/projects/sat/lrat/tests/example-4-vars.cnf
A books/projects/sat/lrat/tests/example-4-vars.lrat
A books/projects/sat/lrat/tests/uuf-100-1.cnf
A books/projects/sat/lrat/tests/uuf-100-1.lrat
A books/projects/sat/lrat/tests/uuf-100-2.cnf
A books/projects/sat/lrat/tests/uuf-100-2.lrat
A books/projects/sat/lrat/tests/uuf-100-3.cnf
A books/projects/sat/lrat/tests/uuf-100-3.lrat
A books/projects/sat/lrat/tests/uuf-100-4.cnf
A books/projects/sat/lrat/tests/uuf-100-4.lrat
A books/projects/sat/lrat/tests/uuf-100-5.cnf
A books/projects/sat/lrat/tests/uuf-100-5.lrat
A books/projects/sat/lrat/tests/uuf-30-1.cnf
A books/projects/sat/lrat/tests/uuf-30-1.lrat
A books/projects/sat/lrat/top.lisp
A books/projects/sat/lrat/truth-monotone.lisp
A books/projects/sat/lrat/unit-propagation-correct.lisp
A books/projects/sat/lrat/unit-propagation-implies-unsat.lisp
A books/projects/sat/lrat/unit-propagation-monotone.lisp

Log Message:
-----------
Merge commit 'a65f5ac8e0238c558071b091daebf947310a0c16' into HEAD


Compare: https://github.com/acl2/acl2/compare/a65f5ac8e023...d2b2cf482564