{"push_id":1799800514,"size":9,"distinct_size":9,"ref":"refs/heads/trunk","head":"dcc5064bbc6f01b498abfdf80f0ea13a26381926","before":"f4cec75fe74ff3f66f401efab357cae79124d984","commits":[{"sha":"649cc52200303abe4559d4c501c8aca06eed7591","author":{"name":"Jason Gross","email":"7298f0ef53f11b987e31cc57a2822f169086d0c9@gmail.com"},"message":"[travis overlay] Partially Revert 013c0232953f1f58\n\nI've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/649cc52200303abe4559d4c501c8aca06eed7591"},{"sha":"6332f43dfee3efc890c5f8fdc1b5b54942c16307","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Explicit the unsafe flag of all calls to Refine.refine.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/6332f43dfee3efc890c5f8fdc1b5b54942c16307"},{"sha":"22ca6b0d70bb8b49aaa420f844c75592e5781c21","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Turn the default behaviour of the refine primitive into the safe one.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/22ca6b0d70bb8b49aaa420f844c75592e5781c21"},{"sha":"3cfb38cb0e5491d13a6ef5cda81dfec7f979cced","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Documenting the change of default flag value of Refine.refine.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/3cfb38cb0e5491d13a6ef5cda81dfec7f979cced"},{"sha":"0fad09306982a88ff8d633d36abdc440dd542ab3","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Dualize the unsafe flag of refine into typecheck and make it mandatory.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/0fad09306982a88ff8d633d36abdc440dd542ab3"},{"sha":"d50923b778684a2ffcc211beb5341a54304c97a4","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[print] Allow Selective Printing of Notations\n\nWe add new API to the printer to allows toggling the printing of\nindividual notations and scopes:\n\n```ocaml\nval toggle_scope_printing :\n  scope:Notation_term.scope_name -> activate:bool -> unit\n\nval toggle_notation_printing :\n  ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit\n```\n\nThis API is meant to be used by ML plugins.\n\n[this commit includes some refactoring by EJGA]","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/d50923b778684a2ffcc211beb5341a54304c97a4"},{"sha":"9a3aba3677686c1e93a04e27f94414c0d6643c42","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/9a3aba3677686c1e93a04e27f94414c0d6643c42"},{"sha":"aed7a86b2147e70bebd50a4d19bac33908da334b","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR#703: New version of the selective-unfolding PR","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/aed7a86b2147e70bebd50a4d19bac33908da334b"},{"sha":"dcc5064bbc6f01b498abfdf80f0ea13a26381926","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR#622: Change the default flag value for Refine.refine","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/dcc5064bbc6f01b498abfdf80f0ea13a26381926"}]}
{"actor":{"display_login":"coqbot"}}