GitHub PushEvent at 2014-07-10 18:08:14
Repository: lean-osx
Actor: soonhokong
Payload: {"shas":[["43eba857cb3502fc2e545741823ef690a0f46a49","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["aff766430d8f2822abd05a0f29cbf1895d3d41aa","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(frontends/lean/pp): universe pretty printer\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["0ec6fa02debadc832b03668d9031b03ee12a84e9","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean/pp_options): remove the 'lean.' prefix\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["12d89ea0b96710f27737639889379bf97a1a8a07","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(kernel/level): is_geq predicate\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["d9b2801eebe64e03acb39ac97634413c02fe7f8a","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean): use the same universe in declarations such as (A B : Type)\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["313c7066e7f40181ae519234e9b19505ff162157","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean): add Type' as notation for Type.{_+1}\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["1a6d0784f2e52a3df66e1dae2c77c96be4d28a7f","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(kernel/level): improve universe level normalization procedure\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["fc8ddcb0ce5821e0829e011c1a9e46368b624193","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean): improve 'check' command when used inside sections\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["49bc3fffbd4e7b933ad654bbe3276d405fc1ccb6","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(frontends/lean/pp): purify procedure for local names\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["06beff327fd71c8c6875860c76549d2ab142c6ec","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","test(tests/lean/run): add more universe tests\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["c13c75b93e5839becb602116d13e1302a39abd12","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean/pp): add option for displaying fully qualified names\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["92bb0468547ad460215e76adbec1b72bcbe355b6","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","test(tests/lean/run): add nested let-expr test\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["405e57eb2d7bd7aaabcf27d39136ed58b659555c","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","refactor(kernel/formatter): add formatter_factory, and simplify formatter interface\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["6af7e7f7947ba6c3c2790cb3b2cfb9b607e227bd","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(kernel/expr_eq_fn): take local pp name into account when annotations are considered in the equality test\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["b62abf0f0630ede920c4315c854bf4040cc5ad75","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","refactor(library/tactic/goal): remove redundance, goal pp method was duplicating some of the functionality provided by the pretty printer\n\nSigned-off-by: Leonardo de Moura <leonardo@microsoft.com>","Leonardo de Moura",true],["d3b1e1127e7ffa0f8488fbcf8fc3a0d75d672d04","1b60d2ed7158736cbc1353d72a6dc44a6772147f@travis-ci.org","refactor(library/tactic/goal): remove redundance, goal pp method was duplicating some of the functionality provided by the pretty printer","Travis CI",true]],"size":16,"ref":"refs/heads/master","head":"d3b1e1127e7ffa0f8488fbcf8fc3a0d75d672d04"}