{"push_id":1182573958,"size":12,"distinct_size":12,"ref":"refs/heads/master","head":"0d359861c57201f707eec715395234aa9d3cb645","before":"2c5bd4162083c5df623e8ffded69c09897edbbb9","commits":[{"sha":"23be0bee4ddc926e0fc7cb7737c5eb22085ec4b1","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"Put Empty and Unit in Type0","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/23be0bee4ddc926e0fc7cb7737c5eb22085ec4b1"},{"sha":"94f346772914aba55a1174b6517fe88e9b3a52ef","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"better fix for exercise","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/94f346772914aba55a1174b6517fe88e9b3a52ef"},{"sha":"b9180e8582d8f24c5546b80ea8e742db29e280d0","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"remove unnecessary type annotations","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/b9180e8582d8f24c5546b80ea8e742db29e280d0"},{"sha":"61174afdf9315d5ef27362e29d8cb1c7c2d7bf48","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"inline proof of inO_iff_isnull","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/61174afdf9315d5ef27362e29d8cb1c7c2d7bf48"},{"sha":"93e05e11aac7efbbc927e21c220e7a0a39a84322","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"remove unnecessary annotations","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/93e05e11aac7efbbc927e21c220e7a0a39a84322"},{"sha":"b799bb885c5fc74db424133a868ffebdeb078b87","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"cleaner definition for inO_iff_isnull in Modalities.Open","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/b799bb885c5fc74db424133a868ffebdeb078b87"},{"sha":"115cd55cbe5f1b8f2b48d9257a6526c05f8c5caf","author":{"name":"Bas Spitters","email":"0935ca057390fbdd683aa138b99a5584e451808e@gmail.com"},"message":"Update Modality.v (#814)\n\nThe localization file has moved.","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/115cd55cbe5f1b8f2b48d9257a6526c05f8c5caf"},{"sha":"3c56b1f4b2531987e8c79f5e01decb7ab4940a55","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"add reference to Coq bug #4862","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/3c56b1f4b2531987e8c79f5e01decb7ab4940a55"},{"sha":"94b68eab61ddf1f0953448db1b13b675f3603ab3","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"annotate isequiv_unit_name to produce an error if the number of universes changes","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/94b68eab61ddf1f0953448db1b13b675f3603ab3"},{"sha":"14ae4c2e7becb46abb4bfaf5008c385830c30a92","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"talk about binder phantom universes in STYLE.md","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/14ae4c2e7becb46abb4bfaf5008c385830c30a92"},{"sha":"2b41e14543584983737f1fc8977eac5924d9b727","author":{"name":"Jason Gross","email":"7298f0ef53f11b987e31cc57a2822f169086d0c9@gmail.com"},"message":"Merge pull request #813 from SkySkimmer/empty-unit-in-type0-no-minim\n\nPut Empty and Unit in Type0","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/2b41e14543584983737f1fc8977eac5924d9b727"},{"sha":"0d359861c57201f707eec715395234aa9d3cb645","author":{"name":"Jason Gross","email":"7298f0ef53f11b987e31cc57a2822f169086d0c9@gmail.com"},"message":"Mention bug #4868","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/HoTT/commits/0d359861c57201f707eec715395234aa9d3cb645"}]}
{"actor":{"display_login":"SkySkimmer"}}