{"push_id":1863886702,"size":9,"distinct_size":9,"ref":"refs/heads/stronger-kernel-types","head":"e3a990176ce5a90d742a6c7bea195a617dc20a3d","before":"80fba6c63bfe53cbe765a0808479de9f27659750","commits":[{"sha":"839e87fffdf2634b841aeba6de6d36a2d7a27dbd","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"Remove some useless code in Term_typing\n\nThe [let _typ = ...] comes from before universe polymorphism. In those\ntimes it was [let _typ, cst = ...] which produced something of use.\n\nThe asserts come from 359e4ffe3 and before (2006 and before). In those\ntimes [Typeops.infer] rebuilt the term being typed, but nowadays the\nassert seems of little use.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/839e87fffdf2634b841aeba6de6d36a2d7a27dbd"},{"sha":"a2bc4d3be684ad24ea7888df4dd0cf35d9733c64","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"Remove dead code [Universes.simplify_universe_context]\n\nDead since 23f4804b50307766219392229757e75da9aa41d9","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/a2bc4d3be684ad24ea7888df4dd0cf35d9733c64"},{"sha":"eba5d64fee0bf6235265f1f6cc884b4cbefe2704","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR #783: Remove some useless code in Term_typing","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/eba5d64fee0bf6235265f1f6cc884b4cbefe2704"},{"sha":"0315a5d93c2de996f5c91bd2af827d3984ec1ad8","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR #781: Remove dead code [Universes.simplify_universe_context]","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/0315a5d93c2de996f5c91bd2af827d3984ec1ad8"},{"sha":"5e246da8e25a766c120d6eb027d8dd77ba2fe804","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"More precise type for universe entries.\n\nWe use an algebraic type instead of a pair of a boolean and the corresponding\ndata. For now, this is isomorphic, but this allows later change in the structure.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/5e246da8e25a766c120d6eb027d8dd77ba2fe804"},{"sha":"5f22136181ecc1603e6e0fccdfec731efcf8e252","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Using a record type for Cooking.result.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/5f22136181ecc1603e6e0fccdfec731efcf8e252"},{"sha":"8e10a24c62c56b35c8534e29c67848e528bfdc02","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"More precise type of entries capturing their lack of side-effects.\n\nWe sprinkle a few GADTs in the kernel in order to statically ensure that\nentries are pure, so that we get stronger invariants.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/8e10a24c62c56b35c8534e29c67848e528bfdc02"},{"sha":"6a50a6b7443446bd037694b9e031914dba79ee12","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Remove a horrendous hack in Declare to retrieve exported side-effects.\n\nInstead of relying on a mutable state in the object pushed on the libstack,\nwe export an API in the kernel that exports the side-effects of a given\nentry in the global environment.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/6a50a6b7443446bd037694b9e031914dba79ee12"},{"sha":"e3a990176ce5a90d742a6c7bea195a617dc20a3d","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Further simplication: do not recreate entries for side-effects.\n\nThis is actually useless, the code does not depend on the value of the\nentry for side-effects.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/e3a990176ce5a90d742a6c7bea195a617dc20a3d"}]}
{"actor":{"display_login":"ppedrot"}}