{"push_id":1068000841,"size":1000,"distinct_size":214,"ref":"refs/heads/trunk","head":"a88f5f162272ced5fb2b8ea555756b8fc51b939a","before":"2bb05717bde540332aa814a59da3745f2097dedf","commits":[{"sha":"cd9a2e9e59d87801790859ddd26d225d71be7f7c","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Fixing test-suite","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/cd9a2e9e59d87801790859ddd26d225d71be7f7c"},{"sha":"f8658b06b98e59e7f6397c6082e4b9b399499948","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Fixing bug #4366: Conversion tactics recheck uselessly convertibility.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/f8658b06b98e59e7f6397c6082e4b9b399499948"},{"sha":"303694c6436b36b114f4919ad7cacc9c053d11a3","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Adding test for bug #4366.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/303694c6436b36b114f4919ad7cacc9c053d11a3"},{"sha":"c1ebc07204c65b4570333748b63a3ef60618b026","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Gather VM tags in Cbytecodes.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/c1ebc07204c65b4570333748b63a3ef60618b026"},{"sha":"a479aa6e8dbd1dda1af2412f8c1e1ff40f0d5a0b","author":{"email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org","name":"Matthieu Sozeau"},"message":"Fix rechecking of applications: it can be given ill-typed terms. Fixes math-classes.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/a479aa6e8dbd1dda1af2412f8c1e1ff40f0d5a0b"},{"sha":"b9a3925288af0cf3023c9a0073dc1eb295270de8","author":{"email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org","name":"Matthieu Sozeau"},"message":"Fix Definition id := Eval <redexpr> in by passing the right universe\ncontext to the reduction function. Fixes MapleMode.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/b9a3925288af0cf3023c9a0073dc1eb295270de8"},{"sha":"50183ce7200d6059b4146c0cc4933aa524178c02","author":{"email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org","name":"Matthieu Sozeau"},"message":"Univs: be more restrictive for template polymorphic constants: only\ndirect aliases are ok, and indices should not be made polymorphic. Fixes NFix.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/50183ce7200d6059b4146c0cc4933aa524178c02"},{"sha":"26974a4a2301cc7b1188a3f2f29f3d3368eccc0b","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Remove code that was already commented out.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/26974a4a2301cc7b1188a3f2f29f3d3368eccc0b"},{"sha":"10e5883fed21f9631e1aa65adb7a7e62a529987f","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Merge branch 'v8.5'","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/10e5883fed21f9631e1aa65adb7a7e62a529987f"},{"sha":"ed95f122f3c68becc09c653471dc2982b346d343","author":{"email":"43f1ac15e1612ec31474d70389158936df20a6d4@inria.fr","name":"Guillaume Melquiond"},"message":"Fix some typos.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/ed95f122f3c68becc09c653471dc2982b346d343"},{"sha":"f617aeef08441e83b13f839ce767b840fddbcf7d","author":{"email":"43f1ac15e1612ec31474d70389158936df20a6d4@inria.fr","name":"Guillaume Melquiond"},"message":"Fix some typos.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/f617aeef08441e83b13f839ce767b840fddbcf7d"},{"sha":"4a1234459472c5fbb0d0467217972f247c054832","author":{"email":"43f1ac15e1612ec31474d70389158936df20a6d4@inria.fr","name":"Guillaume Melquiond"},"message":"Remove some unused variables.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/4a1234459472c5fbb0d0467217972f247c054832"},{"sha":"bc1c530550e7d06655d541c21859321a2f84c260","author":{"email":"43f1ac15e1612ec31474d70389158936df20a6d4@inria.fr","name":"Guillaume Melquiond"},"message":"Make interpreter of PROJ simpler by not using the stack.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/bc1c530550e7d06655d541c21859321a2f84c260"},{"sha":"d024277d485e3b6a70c217be965063a66aeffefe","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Fixing bug #4367: Wrong error message in unification.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/d024277d485e3b6a70c217be965063a66aeffefe"},{"sha":"043d67c93111328fdbc2d7afa1a84daf3d68a5cc","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Remove unused infos structure in VM.\n\nBecame unused after c47b205206d832430fa80a3386be80149e281d33.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/043d67c93111328fdbc2d7afa1a84daf3d68a5cc"},{"sha":"f45a88ad054b88792ec8cc6631e4d4015fa95bab","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Remove -vm flag of coqtop.\n\nUsed to replace the standard conversion by the VM. Not so useful, and\nimplemented using a bunch of references inside and outside the kernel.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/f45a88ad054b88792ec8cc6631e4d4015fa95bab"},{"sha":"0f74b3df6e64dc069e53c4afcd6f46129b211d09","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Remove reference to default conversion function inside the kernel.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/0f74b3df6e64dc069e53c4afcd6f46129b211d09"},{"sha":"4b8155591be6e20505ee25f7199edcf44a638c7e","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Fixing evarmap implementation.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/4b8155591be6e20505ee25f7199edcf44a638c7e"},{"sha":"36f669f769fa23eb897adfa0450875a3c0db3476","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Exporting the original unprocessed hint in the hint running function.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/36f669f769fa23eb897adfa0450875a3c0db3476"},{"sha":"db80daaf82a08a1475c65f7c82bffb63c7efd27a","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Temporary fix: kernel conversion needs to ignore l2r flag.\n\nStdlib does not compile when l2r flag is actually taken into account. We should\ninvestigate...","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/db80daaf82a08a1475c65f7c82bffb63c7efd27a"}]}