{"push_id":4056763884,"size":80,"distinct_size":6,"ref":"refs/heads/sections-stack-in-kernel","head":"3120abbe8f77faec669fa0c101835c62e59a9eee","before":"4e36f6c063d49c86e9c9e362bbab41d31564e332","commits":[{"sha":"bb64d76f9fe80ecdef4f09c797914022783ccb80","author":{"name":"Kazuhiko Sakaguchi","email":"6c0b7b3ea7689927f4d76267fee43479c49b2e39@peano-system.jp"},"message":"Fix #7348: extraction of dependent record projections\n\n- Inline record projections by default (except for Haskell extraction).\n- Extend `pp_record_proj` for record projections involving `MLmagic`.\n- Remove special treatments for pretty-printing for record projections other\n  than `pp_record_proj`.\n- `micromega.ml` had to be changed due to this change of the extraction plugin.\n\nAcknowledgement: This work is financially supported by Peano System Inc.\n\non-behalf-of: @peano-system <info@peano-system.jp>","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/bb64d76f9fe80ecdef4f09c797914022783ccb80"},{"sha":"9b7816a80c77d7f9b4cea35f8ed983763bd8a5c7","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[toplevel] Make all argument lists to be in user-declared order.\n\nAs reported by Karl Palmskog, some lists of arguments were supposed to\nappear in reverse order whereas others do appear in the natural order\nthey are declared.\n\nGiven that in some cases, such as require, order is quite important,\nwe make the parsing return lists in the right order so clients don't\nhave to care about doing `List.rev`.","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/9b7816a80c77d7f9b4cea35f8ed983763bd8a5c7"},{"sha":"6a90e74a59d7848ef1b026533ee600511a1c41ff","author":{"name":"Kazuhiko Sakaguchi","email":"6c0b7b3ea7689927f4d76267fee43479c49b2e39@peano-system.jp"},"message":"Add a changelog entry\n\nAcknowledgement: This work is financially supported by Peano System Inc.\n\non-behalf-of: @peano-system <info@peano-system.jp>","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/6a90e74a59d7848ef1b026533ee600511a1c41ff"},{"sha":"970404f2bfa7a26ad64692844441261cebd80082","author":{"name":"Kazuhiko Sakaguchi","email":"6c0b7b3ea7689927f4d76267fee43479c49b2e39@peano-system.jp"},"message":"[extraction] Fix #7191: Avoid unsound eta-reduction\n\n`Mlutil.simpl` and `Mlutil.atomic_eta_red` did some unsound eta-reductions as\nfollows:\n(fun x0 ... xn => MLexn x0 ... xn)  ->eta  MLexn.\n\n`MLexn` raises an exception thus is not a value in OCaml. So the above\nsimplification may change the behavior of extracted programs. This patch\nrestricts `atomic_eta_red` to eta-redexes whose core is both atomic and value.\n\nAcknowledgement: This work is financially supported by Peano System Inc.\n\non-behalf-of: @peano-system <info@peano-system.jp>","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/970404f2bfa7a26ad64692844441261cebd80082"},{"sha":"5fd3709f00fdb59e8927bb886e09ea4dd00323d0","author":{"name":"Oliver Nash","email":"a5f9e832049bc15c5c5569212bf5fd8572cec019@gmail.com"},"message":"New lemmas for List.v\n\n * filter_app (moved from MSets/MSetRBT.v)\n * filter_map\n * filter_ext_in\n * ext_in_filter\n * filter_ext_in_iff\n * filter_ext\n * concat_filter_map\n * combine_nil\n * combine_firstn_l\n * combine_firstn_r\n * combine_firstn\n * nodup_fixed_point","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/5fd3709f00fdb59e8927bb886e09ea4dd00323d0"},{"sha":"409ba5c818ad17caff37d111e8a1122a145bf70b","author":{"name":"Oliver Nash","email":"a5f9e832049bc15c5c5569212bf5fd8572cec019@gmail.com"},"message":"Apply suggestions from code review\n\nCo-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/409ba5c818ad17caff37d111e8a1122a145bf70b"},{"sha":"c053787e4bdfc28711b0c92416ff3afdca4aecf5","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[ci] Update to OCaml 4.08.1","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/c053787e4bdfc28711b0c92416ff3afdca4aecf5"},{"sha":"3e339284060b4fb3ca6d5c86e354615a4941eca9","author":{"name":"Maxime Dénès","email":"729aee223f7fb2b958d2bed8a43ef191a9e9072b@inria.fr"},"message":"Logic monad debug printer now emits a debug message","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/3e339284060b4fb3ca6d5c86e354615a4941eca9"},{"sha":"1e6fb6005ef98d1709b09adfcb0726da2fc8b7f4","author":{"name":"Maxime Dénès","email":"729aee223f7fb2b958d2bed8a43ef191a9e9072b@inria.fr"},"message":"Remove wrong advice to base feedback level choice on encoding issues","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/1e6fb6005ef98d1709b09adfcb0726da2fc8b7f4"},{"sha":"6bc9ef56c5833ee81d7298ab0c52146ad775e2a1","author":{"name":"Maxime Dénès","email":"729aee223f7fb2b958d2bed8a43ef191a9e9072b@inria.fr"},"message":"Make sure that all query commands return a notice (not an info) feedback\n\nAs documented in the feedback API.","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/6bc9ef56c5833ee81d7298ab0c52146ad775e2a1"},{"sha":"2d4033152c51eb0b093c79d19a5146995af1b432","author":{"name":"Maxime Dénès","email":"729aee223f7fb2b958d2bed8a43ef191a9e9072b@inria.fr"},"message":"Fix a few wrong uses of `msg_notice`","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/2d4033152c51eb0b093c79d19a5146995af1b432"},{"sha":"cff295c4bbc796c4d838842795c324601a2a037c","author":{"name":"Andreas Lynge","email":"3ff516f6b30fbb414bedfbfcc699194d9077c9da@gmail.com"},"message":"Make SSR congr tactic work on arrows in Type.\n\nMatthieu Sozeau explained how to fix this.","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/cff295c4bbc796c4d838842795c324601a2a037c"},{"sha":"ea23c93e33131216cff049a908a3e423dc704624","author":{"name":"Yishuai Li","email":"edbb844ad022f82a2752f717a43cbf43825a563e@cis.upenn.edu"},"message":"Vectors: lemmas about uncons and splitAt\n\nCo-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/ea23c93e33131216cff049a908a3e423dc704624"},{"sha":"7ee359556287610fde675f936f74ab3ab37d8e00","author":{"name":"Yishuai Li","email":"edbb844ad022f82a2752f717a43cbf43825a563e@upenn.edu"},"message":"Changelog: more accurate on uncons","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/7ee359556287610fde675f936f74ab3ab37d8e00"},{"sha":"016c22454c6745ac753d7e376c9f457d6e934114","author":{"name":"Yishuai Li","email":"edbb844ad022f82a2752f717a43cbf43825a563e@upenn.edu"},"message":"edits per review","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/016c22454c6745ac753d7e376c9f457d6e934114"},{"sha":"61750abbc38dee8f9299b309979e0382d48ac323","author":{"name":"Maxime Dénès","email":"729aee223f7fb2b958d2bed8a43ef191a9e9072b@inria.fr"},"message":"Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reduction\n\nReviewed-by: maximedenes","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/61750abbc38dee8f9299b309979e0382d48ac323"},{"sha":"671bc2bba6576434bee3be5e0b45d4f1515c7443","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@Inria.fr"},"message":"Merge PR #10719: Make SSR congr tactic work on arrows in Type.\n\nReviewed-by: gares","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/671bc2bba6576434bee3be5e0b45d4f1515c7443"},{"sha":"049142777e3c34faf74081842b2c363dd6462eb0","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Merge PR #10645: [ci] Update to OCaml 4.08.1\n\nAck-by: Zimmi48\nReviewed-by: vbgl\nReviewed-by: SkySkimmer","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/049142777e3c34faf74081842b2c363dd6462eb0"},{"sha":"8b07d47d9115905354b750e4ccc8e3efb29cd831","author":{"name":"Oliver Nash","email":"a5f9e832049bc15c5c5569212bf5fd8572cec019@gmail.com"},"message":"New lemmas for List.v\n\n * filter_app (moved from MSets/MSetRBT.v)\n * filter_map\n * filter_ext_in\n * ext_in_filter\n * filter_ext_in_iff\n * filter_ext\n * concat_filter_map\n * combine_nil\n * combine_firstn_l\n * combine_firstn_r\n * combine_firstn\n * nodup_fixed_point","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/8b07d47d9115905354b750e4ccc8e3efb29cd831"},{"sha":"5beee5423d32ada40de31608c7fd7c57dd9a6f91","author":{"name":"Oliver Nash","email":"a5f9e832049bc15c5c5569212bf5fd8572cec019@gmail.com"},"message":"Apply suggestions from code review\n\nCo-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>","distinct":false,"url":"https://api.github.com/repos/ppedrot/coq/commits/5beee5423d32ada40de31608c7fd7c57dd9a6f91"}]}
{"actor":{"display_login":"ppedrot"}}