{"push_id":3104501465,"size":2,"distinct_size":2,"ref":"refs/heads/proof+no_global_partial","head":"fffaf8d44f3ec1d0cc61f325492ee7b7c2d2dff5","before":"26d243914b6626d59403d4612706ac838e47335c","commits":[{"sha":"2348146eda14ca6749f87d4056418f41e0e6b626","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[vernac] Adapt to removal of imperative proof state.","distinct":true,"url":"https://api.github.com/repos/ejgallego/coq/commits/2348146eda14ca6749f87d4056418f41e0e6b626"},{"sha":"fffaf8d44f3ec1d0cc61f325492ee7b7c2d2dff5","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[coqpp] [ltac] Adapt to removal of imperative proof state.\n\nWe add state handling to tactics.\n\nTODO:\n\n- [rewrite] `add_morphism_infer` creates problems as it opens a proof.\n- [g_obligations] with_tac","distinct":true,"url":"https://api.github.com/repos/ejgallego/coq/commits/fffaf8d44f3ec1d0cc61f325492ee7b7c2d2dff5"}]}
{"actor":{"display_login":"ejgallego"}}