{"push_id":2299188435,"size":8,"distinct_size":8,"ref":"refs/heads/master","head":"76aff3cbe39da657abb1f559b8ba411a49aab317","before":"c658141acff6d1b7f610960dd39998385c7e8806","commits":[{"sha":"779c0bd23bbc0bd1d0c1cb358fe9725e7d7ccc74","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[lib] Respect change of options under with/without_option.\n\nThe old semantics of `with/without_option` allowed the called function\nto modify the value of the option. This is an issue mainly with the\n`silently/verbose` combinators, as `Set Silent` can be executed under\none of them and thus the modification will be lost in the updated code\nintroduced in a554519874c15d0a790082e5f15f3dc2419c6c38\n\nIMHO these kind of semantics are quite messy but we have to preserve\nthem in order for the `Silent` system to work. In fact, note that in\nthe previous code, `with_options` was not consistent with\n`with_option` [maybe that got me confused?]\n\nIdeally we could restore the saner semantics once we clean up the\n`Silent` system [that is, we remove the flag altogether], but that'll\nhave to wait.\n\nFixes #6645.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/779c0bd23bbc0bd1d0c1cb358fe9725e7d7ccc74"},{"sha":"063ea7f22ce7749f0b1d0c62fa37d2450356e7fd","author":{"name":"Paul Steckler","email":"3e28969a28708413e246320f9a89f07a222cf45c@stecksoft.com"},"message":"Delete duplicate line","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/063ea7f22ce7749f0b1d0c62fa37d2450356e7fd"},{"sha":"f1d74986cdd91849c9b86721265c652e1397db02","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[stm] Move options to a per-document record.\n\nWe gather (almost) all the STM options in a record, now set at\ndocument creation time.\n\nThis is refactoring is convenient for some other ongoing\nfunctionalization work.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/f1d74986cdd91849c9b86721265c652e1397db02"},{"sha":"1176d4086b65c79a1d30a55640d3d933fa24a7c1","author":{"name":"Enrico Tassi","email":"a46adc9faf082e84480f72ffaaa22ae593009461@inria.fr"},"message":"Proofview: enter_one: add __LOC__ argument to get relevant error msg\n\nThe type discipline of the tactic monad does not distinguish between\nmono-goal and multi-goal tactics. Unfortunately enter_one \"asserts\nfalse\" if called on 0 or > 1 goals.  The __LOC__:string argument can\nbe used to make the error message more helpful (since the backtrace is\npointless inside the monad).\n\nThe intended usage is \"Goal.enter_one ~__LOC__ (fun gl -> ..\".\n\nThe __LOC__ variable is filled in by the OCaml compiler with the current\nfile name and line number.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/1176d4086b65c79a1d30a55640d3d933fa24a7c1"},{"sha":"8e3aef19711fa6ccbcb2946afdb690c2fc3d900d","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR #6660: [lib] Respect change of options under with/without_option.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/8e3aef19711fa6ccbcb2946afdb690c2fc3d900d"},{"sha":"700c08b1215e11470814ce82e04551ffc00cdfeb","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR #6672: [stm] Move options to a per-document record.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/700c08b1215e11470814ce82e04551ffc00cdfeb"},{"sha":"48eab4964ffe3d87c8036ed3b10563c595838d73","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant error msg","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/48eab4964ffe3d87c8036ed3b10563c595838d73"},{"sha":"76aff3cbe39da657abb1f559b8ba411a49aab317","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR #6670: Delete duplicate line","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/76aff3cbe39da657abb1f559b8ba411a49aab317"}]}
{"actor":{"display_login":"maximedenes"}}