{"push_id":2007221393,"size":1,"distinct_size":1,"ref":"refs/heads/8.6","head":"81ccea586fad94b0c4721ae94635cfac02db3952","before":"23d94b10d3bb7932b56ca5d27839067223386a74","commits":[{"sha":"81ccea586fad94b0c4721ae94635cfac02db3952","author":{"name":"Matthieu Sozeau","email":"385f7ace2b863d21ff523187b1fd442e431592c6@mattam.org"},"message":"Fix a bug in specialize_eqns not doing enough unification\n\nWe now allow convertible constructor parameters in the equalities we simplify.\nThis limitation was resulting in simplify_IH_hyps failing to simplify when it\ncould. Also reworked the way specialize_eqns performs unifications to\navoid (apparently) exponential behavior of unification in presence of\nlet-bound evars when we know the solutions to the evars cannot come from\nthose lets (substitute instead of keeping them in the context).\n\nFix examples accordingly, and cleanup poly_bocquet to use more of funelim.","distinct":true,"url":"https://api.github.com/repos/mattam82/Coq-Equations/commits/81ccea586fad94b0c4721ae94635cfac02db3952"}]}
{"actor":{"display_login":"mattam82"}}