{"push_id":825778946,"size":40,"distinct_size":40,"ref":"refs/heads/master","head":"348bfa41e26f5d0b27f2acc3eb01fb943c1aed1c","before":"0eab09046edb4761bc14352bd67c64adda143373","commits":[{"sha":"9e7424161090bd28edeadfb69356f05583481f3d","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Fixed the XML generation for type-from-decls and struct-subtype-decls\nIn particular, the generated predicate/projections are made part of these\nclasses and XML elements.","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/9e7424161090bd28edeadfb69356f05583481f3d"},{"sha":"211fc60e7eec5dc9078371478c26f0b2cb9a4eeb","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Started fixing Makefile.in to create a better tar file, with a top-level\ndirectory.","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/211fc60e7eec5dc9078371478c26f0b2cb9a4eeb"},{"sha":"c70dec3e9f53b0dcfa744f3c1a3fc6b554fbf245","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Commented out the find-file-hook in pvs-cmds.el until it works better (causes\ninterrupts)","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/c70dec3e9f53b0dcfa744f3c1a3fc6b554fbf245"},{"sha":"b453e8b5dfa054110167fffce8831299b474fed7","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Added strict-compatible? test to predicate-subtype-of? in equalities.lisp","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/b453e8b5dfa054110167fffce8831299b474fed7"},{"sha":"f6e33bf34d9b11e69ce77a7b45405ce814c396c7","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Minor improvements to proofstate info (still incomplete)","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/f6e33bf34d9b11e69ce77a7b45405ce814c396c7"},{"sha":"6e64aa976095d25d566b06e16de7e3b6706f83b3","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Added type-predicates* (struct-sub-recordtype)","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/6e64aa976095d25d566b06e16de7e3b6706f83b3"},{"sha":"d12e895478ff0eba15c127dfab3e9c16d8629d48","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"1. Modified pp* :around (declaration) for the expr-judgement case, where the\n   formals are a flat list.\n2. Added pp* :around (expr-judgement)","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/d12e895478ff0eba15c127dfab3e9c16d8629d48"},{"sha":"e75c2595c6ec1328dc8669dff63f65550014de22","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"The changes below are for a bug reported by NASA where a macro generated an\nunprovable TCC.  The TCC was generated too soon; it needed to be delayed.\nThe details are:\n\n1. Modified set-type* :around (application), set-type-around-name-expr, and\n   check-for-application-macro-tccs* to check *generate-tccs* before dealing with\n   macros; otherwise improper TCCs are generated.  The right ones are generated\n   later, when *generate-tccs* is not 'none\n\n2. Modified set-type-nonboolop-application to handle macros especially","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/e75c2595c6ec1328dc8669dff63f65550014de22"},{"sha":"11424b19cdbd512c4e5e4211018f3d7dc48f8fbd","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Minor fix to latex-proof*","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/11424b19cdbd512c4e5e4211018f3d7dc48f8fbd"},{"sha":"4a8af788592c4972ca50e990872bc79bc673f6c1","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Fixed get-decl-resolutions to check for type-expr? before getting print-type\nin creating the print type for a copy","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/4a8af788592c4972ca50e990872bc79bc673f6c1"},{"sha":"151f17c50c72e7aa54230465169cc0060cfd5021","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"1. Modified subst-params-decl (conversion-decl) to only add the declaration\n   (add-decl) if there are no free variables in the expression\n2. Modified check-compatible-param to use strict-compatible? instead of\n   compatible? in the test","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/151f17c50c72e7aa54230465169cc0060cfd5021"},{"sha":"6adeb0eb28ad196dcd8edcea52ab98e793ad3f2c","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Modified decl-context to put the setting of (current-declaration) outside of\nwith-current-decl, else it won't persist","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/6adeb0eb28ad196dcd8edcea52ab98e793ad3f2c"},{"sha":"7d583e752b842dc90456d77f29ba9e534fc735dc","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Modified disallowed-free-variable? to check if *in-checker* as well","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/7d583e752b842dc90456d77f29ba9e534fc735dc"},{"sha":"66a6c24950d746a3bcb09a9e7be29c12b450bee3","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Fix to tc-eq-adt-ops in equalities.lisp to check for actuals before trying to\nget the positive types.","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/66a6c24950d746a3bcb09a9e7be29c12b450bee3"},{"sha":"9b3fb713de0213bdabc68647b115e2fec8592c3c","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"In list-decls.lisp, added method collect-visible-decl-info* :around\n(adt-def-decl), and modified collect-visible-decl-info* (subtype) to check if\npredicate is a binding-expr before collecting info from the supertype.","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/9b3fb713de0213bdabc68647b115e2fec8592c3c"},{"sha":"2d00e0b7a3834c5c9d1fe8d23362a59ac2e1a657","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Modified copy-slots (name-expr name-expr) in untypecheck.lisp to copy the type\nas well","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/2d00e0b7a3834c5c9d1fe8d23362a59ac2e1a657"},{"sha":"a054df6d9ad30203866a8a7ba8113708ed252d7d","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Fixed decl-context in utils.lisp, which wasn't hadling prelude theories\ncorrectly, plus some fixes related to macros and pvs-meta-info","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/a054df6d9ad30203866a8a7ba8113708ed252d7d"},{"sha":"5c5c6f0771402031c50f467e7b45748f58d16c54","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Fixes for macros, delaying TCC generation till *generate-tccs* is not none","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/5c5c6f0771402031c50f467e7b45748f58d16c54"},{"sha":"44440f32c128804931a0a473fc808aeaaf892b2e","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Minor fix","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/44440f32c128804931a0a473fc808aeaaf892b2e"},{"sha":"f5ec4b19f305577c6afc2fdb0e52a973dda91f59","author":{"email":"840c3ba9562fb962bdd14ded96f5567523f4b173@csl.sri.com","name":"Sam Owre"},"message":"Minor fix","distinct":true,"url":"https://api.github.com/repos/Lanozavr/pvs/commits/f5ec4b19f305577c6afc2fdb0e52a973dda91f59"}]}