{"push_id":604213637,"size":20,"distinct_size":20,"ref":"refs/heads/master","head":"39ba4329041251573cef57e57591ea2c4ca2454b","before":"6676b85e09b62e65160c00f964b1f3f3b254b725","commits":[{"sha":"05bc59477f9efe62973a9ff26ad80ac4ff9f3727","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Add Quotable changes to CHANGELOG","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/05bc59477f9efe62973a9ff26ad80ac4ff9f3727"},{"sha":"e39a9a2bc9c104cd97e614f46609fe967491ff7e","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Merge remote-tracking branch 'refs/remotes/origin/wip/tactical' into wip/tactical\n\nConflicts:\n\tCHANGELOG","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/e39a9a2bc9c104cd97e614f46609fe967491ff7e"},{"sha":"02d007871ae62978a5a3343ed13825319cc0cd5c","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Add beginning of elaborator debugging errors","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/02d007871ae62978a5a3343ed13825319cc0cd5c"},{"sha":"8858c1a9a3994b587a822ce06d94ffed98365ed8","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Basic handling of elaborator debugger invocations","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/8858c1a9a3994b587a822ce06d94ffed98365ed8"},{"sha":"b04d0cbcf211943ad07b33ec01debf4e311e5a98","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Minor, minor readability improvement to Fin.idr","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/b04d0cbcf211943ad07b33ec01debf4e311e5a98"},{"sha":"75a9c8fdefcd9557601e0d9e6d8bc78b81620271","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Show hole context and goals in elaborator debug","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/75a9c8fdefcd9557601e0d9e6d8bc78b81620271"},{"sha":"5d5ec50b44c71f5353f5f03c3e16431f6aac1d83","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Properly highlight bound variables in elaborator debug","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/5d5ec50b44c71f5353f5f03c3e16431f6aac1d83"},{"sha":"535346da24fb78ca4520632fd8708b2412871733","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Use Set to remove duplicate constraints","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/535346da24fb78ca4520632fd8708b2412871733"},{"sha":"426d05275e516ba8dc5e1414ac1e37a7f39caa69","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Add provenance flag to unification errors\n\n(not yet populated with any useful data)","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/426d05275e516ba8dc5e1414ac1e37a7f39caa69"},{"sha":"9546bd4531b25363b400df1a7e44fc75550854bd","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Ignore accessibility when rechecking\n\naccess rules (private/public) only relevant during elaboration","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/9546bd4531b25363b400df1a7e44fc75550854bd"},{"sha":"179c7043628c25807fed45c717cd1bc606057b20","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Record provenance of types in 'fill' errors\n\nThis covers unification errors arising from variables and function\napplications (which is a lot of them)","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/179c7043628c25807fed45c717cd1bc606057b20"},{"sha":"3d8745489262e410050c4323e8f2841141e655f5","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"TT pretty-printing - also in elab debug","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/3d8745489262e410050c4323e8f2841141e655f5"},{"sha":"771ae4ae5e330132be49a2a7d49fcdd302e43474","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Make IDE mode default to 70 character terminals","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/771ae4ae5e330132be49a2a7d49fcdd302e43474"},{"sha":"bb013f0df6f742e777ef2a2a911c2b0f90fcb8a7","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/bb013f0df6f742e777ef2a2a911c2b0f90fcb8a7"},{"sha":"75f6c2dc1413425356487b4ab25beebeb2efbf73","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Add :core to the REPL\n\n:core TM shows the elaborated value and type of TM","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/75f6c2dc1413425356487b4ab25beebeb2efbf73"},{"sha":"01c4f2a39c9a9bb391d70e98713d6de16548a67b","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"A bit more unification error provenance","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/01c4f2a39c9a9bb391d70e98713d6de16548a67b"},{"sha":"6c26814d08390b956d8d56806096c8f14955560e","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Add IDE command for showing TT\n\nThis enables interactions in IDEs such as right-clicking terms in error\nmessages to see the corresponding TT terms, similar to the implicits and\nnormalisation commands.","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/6c26814d08390b956d8d56806096c8f14955560e"},{"sha":"ebac0885dbd763ba2d23a5e935e40a35374e3266","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Raymond Christiansen"},"message":"Annotate provenance terms","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/ebac0885dbd763ba2d23a5e935e40a35374e3266"},{"sha":"6d768bb670db3b5ec17ab8655e9f581e71fb3f10","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"More information if a function is overapplied","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/6d768bb670db3b5ec17ab8655e9f581e71fb3f10"},{"sha":"39ba4329041251573cef57e57591ea2c4ca2454b","author":{"email":"aa743a0aaec8f7d7a1f01442503957f4d7a2d634@davidchristiansen.dk","name":"David Christiansen"},"message":"Merge pull request #2002 from david-christiansen/better-fin-error\n\nMinor, minor readability improvement to Fin.idr","distinct":true,"url":"https://api.github.com/repos/tdidriksen/Idris-dev/commits/39ba4329041251573cef57e57591ea2c4ca2454b"}]}