{"push_id":1361528124,"size":5,"distinct_size":5,"ref":"refs/heads/v8.6","head":"f667e270116aaf46f1c27b5a925d3ffaf0d31365","before":"a5b977e3acb6d2cd73ed6c895a7d4b587366caa9","commits":[{"sha":"ecaea9a428c052ea431ec7c392e81aaf918d5d96","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Fix minimization to be insensitive to redundant arcs.\n\nThe new algorithm produces different sets of arcs than in 8.5, hence\nexisting developments may fail to pass now because they relied on\nthe (correct but more approximate) result of minimization in 8.5 which\nwasn't insensitive.\n\nThe algorithm works bottom-up on the (well-founded) graph to\nfind lower levels that an upper level can be minimized to. We\nfilter said lower levels according to the lower sets of the other levels\nwe consider. If they appear in any of them then we don't need their\nconstraints. Does not seem to have a huge impact on performance in HoTT,\nbut this should be evaluated further.\n\nAdapt test-suite files accordingly.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/ecaea9a428c052ea431ec7c392e81aaf918d5d96"},{"sha":"1df663324385c9958df76f3f464b6afab4c17ad7","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Cleanup code according to comments.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/1df663324385c9958df76f3f464b6afab4c17ad7"},{"sha":"6b02759513b1ccc7debe87ad9ae6bc6f1341ff6c","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Remove no longer exported debug printer","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/6b02759513b1ccc7debe87ad9ae6bc6f1341ff6c"},{"sha":"5b0b6c92354c34a4f0d5551f88b16264fb08be5f","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3\n\nThis makes [refine] typecheck the term only once (instead of twice),\n(Qed excluded of course). Fix test-suite file for output of constraints\naccordingly.","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/5b0b6c92354c34a4f0d5551f88b16264fb08be5f"},{"sha":"f667e270116aaf46f1c27b5a925d3ffaf0d31365","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Merge branch 'fixminimization' into v8.6","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/f667e270116aaf46f1c27b5a925d3ffaf0d31365"}]}
{"actor":{"display_login":"coqbot"}}