{"push_id":657410566,"size":29,"distinct_size":3,"ref":"refs/heads/master","head":"5e239ba649fce3d29e921eacb7daa12d7589de93","before":"375c9863bfb05b8f8aff03da1f58d5bab5877842","commits":[{"sha":"173703d2b7468f27da988b5576cf844c0b0f5d88","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Added new (co)record syntax.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/173703d2b7468f27da988b5576cf844c0b0f5d88"},{"sha":"6f0aff3e22274d4418c4c34b25bfabc276a5cbe9","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Updated standard library to new record syntax.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/6f0aff3e22274d4418c4c34b25bfabc276a5cbe9"},{"sha":"681d876dfdd0b3360a1e6e1df5037da80c2e3ed8","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Merge branch 'master' into agda-style-records","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/681d876dfdd0b3360a1e6e1df5037da80c2e3ed8"},{"sha":"b5372b52e15971c750950a5c5e2fbe8e39f715c9","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Removed argument customization for now.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/b5372b52e15971c750950a5c5e2fbe8e39f715c9"},{"sha":"aca1148ceb1e25128f4b1fb6e2a6d168a1afbd6c","author":{"email":"a5f5581ec07ceac64309f7cc7fdc557a90b876c9@gmail.com","name":"tdidriksen"},"message":"Merge branch 'master' into agda-style-records\n\nConflicts:\n\tlibs/prelude/IO.idr\n\tsrc/Idris/ElabDecls.hs","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/aca1148ceb1e25128f4b1fb6e2a6d168a1afbd6c"},{"sha":"f36a8f7b9a0cd0fbfaac70f1a7bba54daa468694","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Revamped record elaboration.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/f36a8f7b9a0cd0fbfaac70f1a7bba54daa468694"},{"sha":"7e43af7bb7535e9785d96f111013eccd6fbfe401","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Changed libs to new record syntax.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/7e43af7bb7535e9785d96f111013eccd6fbfe401"},{"sha":"7d42ba28d75a28c14865aabf2ed568f7755c5082","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Changed tests for new record syntax.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/7d42ba28d75a28c14865aabf2ed568f7755c5082"},{"sha":"95964635f0e94eee18cdd82cc757b7506913fb75","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Merge branch 'master' into agda-style-records","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/95964635f0e94eee18cdd82cc757b7506913fb75"},{"sha":"4373184fc118dc3256c53de442e2c7f646887b25","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Added records to changelog.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/4373184fc118dc3256c53de442e2c7f646887b25"},{"sha":"bbbe8803c9b8b5c8ce1f50adf5648d6d77dcd66b","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Merged.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/bbbe8803c9b8b5c8ce1f50adf5648d6d77dcd66b"},{"sha":"86bcbbcbf9e3806cdf4d641af675485f49dd3b12","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"Sune Alkærsig"},"message":"Allowed unnamed fields.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/86bcbbcbf9e3806cdf4d641af675485f49dd3b12"},{"sha":"0269d05baea5706fb8f2e6b451e8130bfae6d2a1","author":{"email":"860730236c3755047501ca57c245f0bc105821e1@Sunes-MacBook-Pro.local","name":"Sune Alkaersig"},"message":"More record stuff.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/0269d05baea5706fb8f2e6b451e8130bfae6d2a1"},{"sha":"26dba597f74373d1d4cc9c8e7e69868b8a8fd652","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"sualitu"},"message":"Merge","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/26dba597f74373d1d4cc9c8e7e69868b8a8fd652"},{"sha":"9c13628838371c2733076617ece14636f5006634","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"sualitu"},"message":"Merge branch 'master' into agda-style-records","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/9c13628838371c2733076617ece14636f5006634"},{"sha":"8e112d79eec536186d05da1d9dced6dc02d73fd5","author":{"email":"38c09e6d17f103ddc71e256f1e270ff8753213c3@itu.dk","name":"sualitu"},"message":"Added tests","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/8e112d79eec536186d05da1d9dced6dc02d73fd5"},{"sha":"c1cd201572b43ba5d2e6906bcac533c6163bb84c","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Merge remote-tracking branch 'refs/remotes/upstream/master' into agda-style-records\n\nConflicts:\n\tsrc/Idris/AbsSyntaxTree.hs\n\tsrc/Idris/Elab/Record.hs","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/c1cd201572b43ba5d2e6906bcac533c6163bb84c"},{"sha":"274b6b1366eaff2b31a37acbff9e6e927c1ad315","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Fix test bitrot","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/274b6b1366eaff2b31a37acbff9e6e927c1ad315"},{"sha":"37ebed39bf77d2cc8f3d7d1058077f4e03c64a24","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Don't project record parameters\n\nThey're already in the right form (guaranteed by the types of the other\nprojections), and relying on projecting them means that they must be in\ncanonical form to get things to type check. Without record eta rules,\nthis is somewhat onerous.","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/37ebed39bf77d2cc8f3d7d1058077f4e03c64a24"},{"sha":"0afd6f259408544550c271eb29121a66cc576f3c","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Docs for new record syntax","distinct":false,"url":"https://api.github.com/repos/david-christiansen/Idris-dev/commits/0afd6f259408544550c271eb29121a66cc576f3c"}]}