GitHub PushEvent at 2014-08-28 00:46:28
Repository: lean
Actor: avigad
Payload: {"shas":[["60d5e87a66d2564966e39dafe60d78721e0628f3","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","test(tests/lean/run): add matrix test\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["42a8fb5965b7ee83ddb183f2acfae6add05f65f3","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","chore(tests/lean/run/matrix): simplify same_dim_irrel proof\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["82a7de83cc338c6ad1262813c2bef76a819f9df0","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean/pp_options): use a more effective get_distinguishing_pp_options\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["4a9e48d249442fdf0946ba79eaee28ef02e1f1fe","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(doc/authors.md): update authors.md page\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["04d9eb17d11a26f139f8f5334c16ec29ae625c66","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(kernel/conveter): improve support for proof irrelevant in the converter\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["2c35696fed539be3ce5925124bbf52fe2783c49d","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","chore(README.md): remove link to Lean 0.1\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["800d3bd70a475e8f8184ad292766172cc85cb3fa","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(doc/lean/tutorial): typos\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["3903be34a432e327ef8e53d1a4b038b44df685d5","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean): process theorem statement independently of proof, thus we have the same behavior in sequential and parallel compilation modes, closes #84\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["c11fd6b0d24b25172681395ce2103c079ae77a48","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(tests/lean/run): adjust tests\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["9715d06f4ab5e3eaf8535679feffa6e3dedd3fa8","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(library): minor cleanup, replace 'refl _' with 'rfl', define equivalence relation for sets\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["413517b86d2cd589fac1e69616f08f7fa6215f87","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","fix(library): correct markdown directories, revise defaults for logic and data","Jeremy Avigad",true],["5eedca08ea50c0ac1ac92bd73ed9cc17a95fbd73","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","refactor(library): set up and document standard/classical/hott imports","Jeremy Avigad",true],["99438f0ee0470ee5c412d838958b1f0788c4fc41","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","chore(library): add 'universe polymorphism' to list of extra feat\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["02b7f980b03c10fafa3f6085583fda7d1214110f","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(library/num): bug in to_pos_num, missing test\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["44c597724b942958b48e94bedd253e2b893297b1","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(frontends/lean): fail if theorem type has metavariables after type elaboration (and before proof elaboration)\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["4c9723e5ed30e00b12372475b543549f04242a21","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(library/unifier): assertion violation\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["4ab0dd47005dc7c95a41da1b9d07bd4c8c294caa","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(tests/lean): adjust test to reflect recent changes\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["11711a2409b337771141201aa3bc2fcec1056179","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(util/rb_tree): do not use thread local storage in template when compiling on OSX with clang++ without Boost\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["b8b5a591171c3966fcab5840e5497e306348dce9","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(frontends/lean/info_manager): do not rely on typeid::before, the behavior is a platform specific\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["40e4a1efa97759ec1913528a2b79d7e0de766f0d","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(tests/lua/slow): reduce test size to avoid stackoverflow on OSX when compiling without Boost\n\nSigned-off-by: Leonardo de Moura <leodemoura@cmacslab5.modck.cs.cmu.edu>","Leonardo de Moura",true]],"size":62,"ref":"refs/heads/master","head":"1011a8022c5fe82cfd7446cf77123ca8ac139dfd"}