[acl2/acl2] e47db4: Slightly improve documentation of RESTRICT and TAI...

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: e47db464172a35203805644c3e9a41ee2a03c94c
https://github.com/acl2/acl2/commit/e47db464172a35203805644c3e9a41ee2a03c94c
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict-reference.lisp
M books/kestrel/apt/tailrec-reference.lisp

Log Message:
-----------
Slightly improve documentation of RESTRICT and TAILREC.

Avoid the appearance of 'ACL2::' in certain documentation links.


Commit: 5810d8f31ba96f60f7e9806cdc250933a5b72501
https://github.com/acl2/acl2/commit/5810d8f31ba96f60f7e9806cdc250933a5b72501
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict.lisp

Log Message:
-----------
Improve output of RESTRICT transformation.

Avoid the termination hints in the exported function event.


Commit: f13a37e7329a56e36a3b9597b74139f261edb2b7
https://github.com/acl2/acl2/commit/f13a37e7329a56e36a3b9597b74139f261edb2b7
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict.lisp
M books/kestrel/apt/tailrec.lisp
M books/kestrel/apt/top.lisp

Log Message:
-----------
Slightly extend APT documentation.

Add an XDOC topic to collect the transformation implementation topics.


Commit: 811160c51ba4a1f96d379cf4a24fc8811ebe8c9c
https://github.com/acl2/acl2/commit/811160c51ba4a1f96d379cf4a24fc8811ebe8c9c
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict.lisp
M books/kestrel/apt/tailrec.lisp

Log Message:
-----------
Slightly improve the output of APT transformations.

With the :SHOW-ONLY T option, print the event form starting at the first column,
instead of returning it as value of an error triple.


Commit: 4dd6d9e6423928355c879df8769527e2c9e9d64c
https://github.com/acl2/acl2/commit/4dd6d9e6423928355c879df8769527e2c9e9d64c
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict.lisp
M books/kestrel/apt/tailrec.lisp

Log Message:
-----------
Improve theorem names generated by APT transformations.

Now the symbol that names the theorem is in the same package as the symbol that
names the target function.


Commit: 7de1f8e7abc3a2ac76c82e85d71cf00a74594c69
https://github.com/acl2/acl2/commit/7de1f8e7abc3a2ac76c82e85d71cf00a74594c69
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/package.lsp

Log Message:
-----------
Add ACL2::ADD-SUFFIX-TO-FN to APT package.


Commit: 6bf61d3c2364de05b6cdb46f10be41924e2e4714
https://github.com/acl2/acl2/commit/6bf61d3c2364de05b6cdb46f10be41924e2e4714
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/tailrec.lisp

Log Message:
-----------
Improve wrapper name generated by TAILREC transformation.

Now the symbol that names the wrapper function is in the same package as the
symbol that names the new function.


Commit: 78bf414ca4fead85840d7ffb5bd9b1992957c0ad
https://github.com/acl2/acl2/commit/78bf414ca4fead85840d7ffb5bd9b1992957c0ad
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/utilities/named-formulas.lisp

Log Message:
-----------
Improve output of named formula utilities.

Each piece of information (when in verbose mode) starts with a blank line and is
followed by no blank line. (Before, it started with no blank line and ended with
a blank line.) This seems more in line with ACL2's general output; the
information being printed by these utility is text(-like).


Commit: 431611673dab618d513216458b5bbe0d74383998
https://github.com/acl2/acl2/commit/431611673dab618d513216458b5bbe0d74383998
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict.lisp
M books/kestrel/apt/tailrec.lisp

Log Message:
-----------
Slightly improve output of APT transformations.

Now the forms for the generated events are printed without any blank lines
around them. The text-like messages for verbose output are printed with a
starting blank line and no ending blank line.


Commit: fe1aa644b992c95e85470f9b2b57019fd75afc58
https://github.com/acl2/acl2/commit/fe1aa644b992c95e85470f9b2b57019fd75afc58
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-04 (Fri, 04 Aug 2017)

Changed paths:
M books/kestrel/apt/package.lsp
M books/kestrel/apt/restrict.lisp

Log Message:
-----------
Add ACL2::TESTS-AND-CALL to APT package.


Commit: e3de551dc28d5b9aca8892cb1893bf327f8d1a11
https://github.com/acl2/acl2/commit/e3de551dc28d5b9aca8892cb1893bf327f8d1a11
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-06 (Sun, 06 Aug 2017)

Changed paths:
M books/acl2s/cgen/build-enumcalls.lisp
M books/acl2s/cgen/cert.acl2
M books/acl2s/cgen/testing-regression.lsp
M books/acl2s/cgen/top.lisp
M books/acl2s/mode-acl2s-dependencies.lisp

Log Message:
-----------
Merge branch 'master'.


Compare: https://github.com/acl2/acl2/compare/630b5161479d...e3de551dc28d

[GitHub]

Branch: refs/heads/master