{"push_id":2908005014,"size":3,"distinct_size":1,"ref":"refs/heads/combined-scheme","head":"5ea3d1b1e01f56573e72d7818a4b7e6393ffdfa8","before":"03f27ccc461e6d7b04efc8a6ec586be504054581","commits":[{"sha":"5780336e3be522f76906b719c3d3694f243a5bdb","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Fixes #8215 (\"critical\" bug of type inference in interpreting evars by names).\n\nWhen interpreting an existential variable \"?n@{inst}\" in the current\ncontext, check that variables bound to local definitions are replaced\nby variables with convertible body.\n\nAlso give a message explaining the type error or non-convertibility\nerror rather than wrongly saying that there is no binding for the\nvariable.","distinct":false,"url":"https://api.github.com/repos/TheoWinterhalter/coq/commits/5780336e3be522f76906b719c3d3694f243a5bdb"},{"sha":"b7cd70b5732d43280fc646115cd8597f2e844f95","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Merge PR #8217: Fixes #8215: \"critical\" type inference bug in interpreting evars by name","distinct":false,"url":"https://api.github.com/repos/TheoWinterhalter/coq/commits/b7cd70b5732d43280fc646115cd8597f2e844f95"},{"sha":"5ea3d1b1e01f56573e72d7818a4b7e6393ffdfa8","author":{"name":"Théo Winterhalter","email":"2f116f526448bec65094a5ac6d2d334225369e2c@gmail.com"},"message":"Combined Scheme tests sort to use either \"*\" or \"/\\\"\n\nAnd update documentation.","distinct":true,"url":"https://api.github.com/repos/TheoWinterhalter/coq/commits/5ea3d1b1e01f56573e72d7818a4b7e6393ffdfa8"}]}
{"actor":{"display_login":"TheoWinterhalter"}}