{"push_id":1344713968,"size":22,"distinct_size":8,"ref":"refs/heads/v8.5+tentative-fix-5097","head":"0af5c4d87b300e93c85b4a1983774c3ef7dce431","before":"c5543c997bd74fc0edd161ef59c5e630ea77f2b7","commits":[{"sha":"e6a054695a2f5d8be3f695975464f99571a69b75","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Ensuring that the evar name is preserved by \"rename\" as it is already\nthe case for clear and the conversion tactics.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/e6a054695a2f5d8be3f695975464f99571a69b75"},{"sha":"4e93587fd83bab4ad5c158aa6b3c194e8a7a5551","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing #4887 (confusion between using and with in documentation of firstorder).","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/4e93587fd83bab4ad5c158aa6b3c194e8a7a5551"},{"sha":"9b1c4576d89014d686bc10f13455a52de8d793bf","author":{"name":"Théo Zimmermann","email":"60470865aec7c618d4abc256c9bdb795474da0a5@gmail.com"},"message":"Make error message more helpful.\n\nCoqIDE does not have a \"display\" menu. It has a \"view\" menu with a list of display options.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/9b1c4576d89014d686bc10f13455a52de8d793bf"},{"sha":"4e3d4646788c96f16193df14a81aa79938812194","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Fix a bug in subst releaved by an OCaml warning.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/4e3d4646788c96f16193df14a81aa79938812194"},{"sha":"844b076bf5150a107d31cd4648955c3a6538a34b","author":{"name":"Cyprien Mangin","email":"f8360d742f8012d00b6eea992cbcdaa81937a9d7@m4x.org"},"message":"Fix #4762.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/844b076bf5150a107d31cd4648955c3a6538a34b"},{"sha":"7952c15ca3d26ae5c2807196bb7aca97bce325c6","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge branch '4762' into v8.5\n\nWas PR#293: Fix #4762 (eauto weaker than auto).","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/7952c15ca3d26ae5c2807196bb7aca97bce325c6"},{"sha":"e74c2e3df2ed40b6df34255f6638a93deb35f434","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge remote-tracking branch 'github/pr/294' into v8.5\n\nWas PR#294: Make error message more helpful.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/e74c2e3df2ed40b6df34255f6638a93deb35f434"},{"sha":"c78af970e1f003587fba9bebdf3ab5ca3b23face","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Fix test-suite.\n\nRestore subst output test file modified by mistake.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/c78af970e1f003587fba9bebdf3ab5ca3b23face"},{"sha":"89ec88f1e750cfb786de1929ef44fac70c9a29ab","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Quick fix to another bug of \"subst\" introduced in 4e3d464 and spotted by Maxime.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/89ec88f1e750cfb786de1929ef44fac70c9a29ab"},{"sha":"14f8db195021e709734ed89d9cb513d1c0db6a93","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing #4970 (confusion between special \"{\" and non special \"{{\" in notations).","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/14f8db195021e709734ed89d9cb513d1c0db6a93"},{"sha":"0b417c12eb10bb29bcee04384b6c0855cb9de73a","author":{"name":"Matthieu Sozeau","email":"451d3b825623fdfe0dafc0e4827303e73a984a0e@inria.fr"},"message":"unification.ml: fix for bug #4763, unif regression\n\nDo not force all remaining conversions problems to be solved after the\n_first_ solution of an evar, but only at the end of assignment of terms\nto evars in w_merge. This was hell to track down, thanks for the help of\nMaxime. contribs pass and HoTT too.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/0b417c12eb10bb29bcee04384b6c0855cb9de73a"},{"sha":"08f4cfc9dfb03973ae652ef6576342ae38f8f199","author":{"name":"Matthieu Sozeau","email":"451d3b825623fdfe0dafc0e4827303e73a984a0e@inria.fr"},"message":"w_merge: Add a comment about the (List.rev evars)\n\nThis change exposed bug #4763","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/08f4cfc9dfb03973ae652ef6576342ae38f8f199"},{"sha":"0a6f0c161756a1878dd81e438df86f08631d8399","author":{"name":"Matthieu Sozeau","email":"451d3b825623fdfe0dafc0e4827303e73a984a0e@inria.fr"},"message":"evarconv.ml: Fix bug #4529, primproj unfolding\n\nEvarconv was made precociously dependent on user-declared reduction\nbehaviors. Only cbn should rely on that.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/0a6f0c161756a1878dd81e438df86f08631d8399"},{"sha":"eb87cdaeb252d758b6a76b36867254823169576b","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).\n\nMore precisely, commands that calls parse_entry put the lexer in an\ninconsistent state, breaking the lexing of bullet which relies on it.\n\n(Not to be pushed to v8.6 which has a better fix).","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/eb87cdaeb252d758b6a76b36867254823169576b"},{"sha":"c70fe0c63238128a6bb98b9fa75445c4b71c7af5","author":{"name":"Arnaud Spiwack","email":"a6a02a54042c1400b77a9dbc2a1b7e9f0dda3490@spiwack.net"},"message":"Fix #4416: - Incorrect \"Error: Incorrect number of goals\"\n\nIn `Ftactic` the number of results could desynchronise with the number\nof goals when some goals were solved by side effect in a different\nbranch of a `DISPATCH`.\n\nSee [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/c70fe0c63238128a6bb98b9fa75445c4b71c7af5"},{"sha":"009718d9d0130a967261ae5d2484985522fc2f7c","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Add test file for #4416.","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/009718d9d0130a967261ae5d2484985522fc2f7c"},{"sha":"b247761476c4b36f0945c19c23c171ea57701178","author":{"name":"Matthieu Sozeau","email":"451d3b825623fdfe0dafc0e4827303e73a984a0e@inria.fr"},"message":"Fix for bug #4863, update the Proofview's env with\n\nside_effects. Partial solution to the handling of side effects\nin proofview.","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/b247761476c4b36f0945c19c23c171ea57701178"},{"sha":"d226adf01f20ea946bbeac4d4c5cde75a4d77f32","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Fix bug #5123: mark all shelved evars unresolvable\n\nPreviously, some splipped through and were caught by unrelated calls to\ntypeclass resolution.","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/d226adf01f20ea946bbeac4d4c5cde75a4d77f32"},{"sha":"6d55121c90ec50319a3de6a6907726fbcdc2f835","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Merge remote-tracking branch 'github/bug4863' into v8.5","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/6d55121c90ec50319a3de6a6907726fbcdc2f835"},{"sha":"2bcae5b7a22019718973f65cafd271f735d3d85b","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Fix test-suite file 5123 to fail in case of regression","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/2bcae5b7a22019718973f65cafd271f735d3d85b"}]}
{"actor":{"display_login":"herbelin"}}