{"push_id":800793998,"size":126,"distinct_size":126,"ref":"refs/heads/letinternal","head":"459290d67f697368d6090f5016e03f77a4110268","before":"cba62f421972cb92fdfbdfd9332edcf9c10221ae","commits":[{"sha":"ce060b7849f601b1d6a8320a7b47e60df584947d","author":{"email":"1294692e88bc3cf578b0cf93126b82e453a3a24f@eafit.edu.co","name":"Andrés Sicard-Ramírez"},"message":"[ Makefile ] Undo unintentional change.\n\nThe master branch doesn't use --program-suffix or\nagda-mode-$(VERSION).","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/ce060b7849f601b1d6a8320a7b47e60df584947d"},{"sha":"ebb616d8edf7177196b5794c1a0977b1d3ebee9a","author":{"email":"dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","name":"Andreas Abel"},"message":"Fixed #1650.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/ebb616d8edf7177196b5794c1a0977b1d3ebee9a"},{"sha":"a7003a01d27bc2230d8ea39a4f27275b05c05c67","author":{"email":"dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","name":"Andreas Abel"},"message":"Merge branch 'maint-2.4.2'\n\nConflicts:\n\tsrc/full/Agda/TypeChecking/CompiledClause/Compile.hs","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/a7003a01d27bc2230d8ea39a4f27275b05c05c67"},{"sha":"d90d44416e60d9bce53ebd2510e03bc6ea6ab44c","author":{"email":"dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","name":"Andreas Abel"},"message":"Fixed #1651.  Adding a REWRITE for a type signature is now an error.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/d90d44416e60d9bce53ebd2510e03bc6ea6ab44c"},{"sha":"90f5641782be6fe502d48b3739cf61e1c21e9a0f","author":{"email":"dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","name":"Andreas Abel"},"message":"Merge branch 'maint-2.4.2'","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/90f5641782be6fe502d48b3739cf61e1c21e9a0f"},{"sha":"b4bd242ef5691001dc398e74b0f2007f75e014f9","author":{"email":"43f2a2d2c86e22bc80f5acc690d97a5dcf4c4b2f@cse.gu.se","name":"Nils Anders Danielsson"},"message":"Removed Agda.Utils.Trie.Lazy, which was unused and rejected by GHC.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/b4bd242ef5691001dc398e74b0f2007f75e014f9"},{"sha":"598af81b87f10dc412404bee719fc727f4d39cff","author":{"email":"43f2a2d2c86e22bc80f5acc690d97a5dcf4c4b2f@cse.gu.se","name":"Nils Anders Danielsson"},"message":"New trie functions: everyPrefix, lookup.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/598af81b87f10dc412404bee719fc727f4d39cff"},{"sha":"73a28d600f383d5097cece7f42ddd018bff15db1","author":{"email":"43f2a2d2c86e22bc80f5acc690d97a5dcf4c4b2f@cse.gu.se","name":"Nils Anders Danielsson"},"message":"Made (many) operator grammars smaller.\n\nThis implies that some error messages become shorter.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/73a28d600f383d5097cece7f42ddd018bff15db1"},{"sha":"2aff828ec9a34ac01eb6954767b9940d7ba81fa0","author":{"email":"43f2a2d2c86e22bc80f5acc690d97a5dcf4c4b2f@cse.gu.se","name":"Nils Anders Danielsson"},"message":"Removed some unused NFData instances.\n\nThese instances were arguably incorrect.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/2aff828ec9a34ac01eb6954767b9940d7ba81fa0"},{"sha":"a80164cd31aea6535de192ed9cd382096126cb72","author":{"email":"43f2a2d2c86e22bc80f5acc690d97a5dcf4c4b2f@cse.gu.se","name":"Nils Anders Danielsson"},"message":"Added or modified many NFData instances.\n\nThese instances do not force ranges.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/a80164cd31aea6535de192ed9cd382096126cb72"},{"sha":"a1be8ad3759a4f3e872b49beca138ec61779502b","author":{"email":"f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","name":"Jesper Cockx"},"message":"[ rewriting ] Added lambdas to the pattern language of rewriting rules\n\nConflicts:\n\tsrc/full/Agda/TypeChecking/Monad/Base/KillRange.hs\n\tsrc/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/a1be8ad3759a4f3e872b49beca138ec61779502b"},{"sha":"a37cc72b327c523cf2eb83e96c515bec728b093e","author":{"email":"f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","name":"Jesper Cockx"},"message":"[ rewriting ] Fix prettyTCM for non-linear patterns (still not very pretty)\n\nConflicts:\n\tsrc/full/Agda/TypeChecking/Pretty.hs","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/a37cc72b327c523cf2eb83e96c515bec728b093e"},{"sha":"69384287f77d5295e2b1a961d68ca9b2ac3bd65c","author":{"email":"f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","name":"Jesper Cockx"},"message":"[ rewriting ] always reduce and eta-contract body when matching against lambda","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/69384287f77d5295e2b1a961d68ca9b2ac3bd65c"},{"sha":"c64ea1472158dcf1d338f87b09701591fae282f3","author":{"email":"f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","name":"Jesper Cockx"},"message":"[ rewriting ] Added pattern for lambda-bound variable applied to arguments\nBound variables do not reduce, so it should be safe to treat them as rigid symbols","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/c64ea1472158dcf1d338f87b09701591fae282f3"},{"sha":"952799cbce16480009a57a9cb4047d6fdffb749c","author":{"email":"f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","name":"Jesper Cockx"},"message":"[ Refactor ] Changed some instances for Type to Type'","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/952799cbce16480009a57a9cb4047d6fdffb749c"},{"sha":"bf2d96c1d660043b9a31b0636467a687819b427d","author":{"email":"f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","name":"Jesper Cockx"},"message":"[ rewriting ] Added a pattern for pi types","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/bf2d96c1d660043b9a31b0636467a687819b427d"},{"sha":"b4b3a50c6292fdeeb4a4e9a4bade12b136e1116b","author":{"email":"f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","name":"Jesper Cockx"},"message":"[ rewriting ] Disambiguate substitution on-the-fly during non-linear matching","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/b4b3a50c6292fdeeb4a4e9a4bade12b136e1116b"},{"sha":"1517f74ab8201ad2ddece317c450277e1f9d4b49","author":{"email":"f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","name":"Jesper Cockx"},"message":"[ rewriting ] Throw mismatch when argument lists have a different length (instead of __IMPOSSIBLE__)","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/1517f74ab8201ad2ddece317c450277e1f9d4b49"},{"sha":"bfebae806e9d41b317675958e0d615d3ca4e3c4d","author":{"email":"dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","name":"Andreas Abel"},"message":"[ rewriting ] Conflict resolution after cherry-picking ho-rewriting to maint.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/bfebae806e9d41b317675958e0d615d3ca4e3c4d"},{"sha":"e6cb239e9090e8a1798609f407bce4e3af36fbd3","author":{"email":"170be567ea0382603d82754ddd57b1c7da053294@gmail.com","name":"Nils Anders Danielsson"},"message":"Failed attempt to exclude private things when applying modules.\n\n+ When the user writes\n\n    open M e <import directive>\n\n  or\n\n    module X = M e <import directive>\n\n  there is little point in including private things in the generated\n  modules, with some exceptions. However, the exceptions are quite\n  important. For instance, consider\n\n    module X = M A using (c),\n\n  where c is a constructor of the datatype D. If we do not include\n  \"D A\" as a private member of X, then we cannot (in general, with the\n  current setup) fill in all the \"Defn\" fields for X.c. This could\n  perhaps be fixed, but there may be other exceptions which I have not\n  thought of, so I will roll back (most of) this patch.","distinct":true,"url":"https://api.github.com/repos/jmchapman/agda/commits/e6cb239e9090e8a1798609f407bce4e3af36fbd3"}]}