GitHub PushEvent at 2014-11-07 14:19:46
Repository: agda
Actor: jespercockx
Payload: {"shas":[["0815be91044d89bf8690c5b82fec544e41c2fbd9","dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","[ clarify ] Removed defacto identity substitution in BasicOps.give.\n\nWhen meta instantiations became open terms in context (instead of\nlambdas), it was not recognized that the application sequence\ncorresponds to the identity substitution.\nhttps://github.com/agda/agda/commit/5e6ffac27d7f37dbe6d9701fcf0feff3d7431827","Andreas Abel",false],["3e3945b3645c2d3bfdddc91010c04d40db777304","dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","[ cosmetics ] and comments.","Andreas Abel",false],["3bc42fa41cf4e3a9b671f9ae55548c0503468488","dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","[ interaction ] Better error message when type checking given expr fails.","Andreas Abel",false],["27e76aea35457731decabedc3447068f31bbb390","dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","[ debug ] printing in Give and checkExpr QuestionMark.","Andreas Abel",false],["e2cf1f5710ee2bd584e67eaeb52e0dc252ee79e0","dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","[ Issue 1342 ] Fixed by outlawing with on module parameter.\n\nThe module free variables should stay free, so no with on them.","Andreas Abel",false],["35e7bee3f98780a94c7e14eeb32cb34a850e4b29","dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","[ Issue 1342 ] Test cases that trigger the new error.","Andreas Abel",false],["2f0ee51c4672b73ab52c624da745b22e2b4eda27","dcc6ca7a371f57bdcd9cd18f3843b0caea4a12fb@ifi.lmu.de","[ Issue 1342 ] CHANGELOG","Andreas Abel",false],["b66f67de625c1a7dc94a2c8d5316a56860724d3f","f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","[ Issue 1345 ] Add context telescope to unquoted clauses before reification.","Jesper Cockx",false],["bb4377c01d202494b66b83ec6dc1a6c9bc0a11ec","f25bb46e8c97531d7c534d4f8dfaab5aad00279c@cs.kuleuven.be","Merge branch 'maint-2.4.2'","Jesper Cockx",true]],"size":9,"ref":"refs/heads/master","head":"bb4377c01d202494b66b83ec6dc1a6c9bc0a11ec"}