{"push_id":680035941,"size":4,"distinct_size":4,"ref":"refs/heads/master","head":"0d1d53e15a6c60f75190b69a3826941636b2b9d4","before":"7f0d9fcd532e7f858e29100fe6384a5ac25b6439","commits":[{"sha":"d31b5e1c3fd69b1d000fe1999f7b02209237d3fa","author":{"email":"f282ad438ecadc93e62523946ab50d77b680b96f@epfl.ch","name":"Samuel Gruetter"},"message":"cp dev/existential/precise-gDot.v dev/existential/CoInd-precise-gDot.v","distinct":true,"url":"https://api.github.com/repos/samuelgruetter/dot-calculus/commits/d31b5e1c3fd69b1d000fe1999f7b02209237d3fa"},{"sha":"9a384b4b319b2b05c47e1f232d5b07325eaffa87","author":{"email":"f282ad438ecadc93e62523946ab50d77b680b96f@epfl.ch","name":"Samuel Gruetter"},"message":"Make CoInductive wf_typ Inductive. As expected, we cannot typecheck recursive types any more, because the wf-ness checks are too deep (we would need an infinite proof tree).","distinct":true,"url":"https://api.github.com/repos/samuelgruetter/dot-calculus/commits/9a384b4b319b2b05c47e1f232d5b07325eaffa87"},{"sha":"f66eb9c8f98d100a7017aaa8568e27213ff5443b","author":{"email":"f282ad438ecadc93e62523946ab50d77b680b96f@epfl.ch","name":"Samuel Gruetter"},"message":"add assumption set to wf judgment","distinct":true,"url":"https://api.github.com/repos/samuelgruetter/dot-calculus/commits/f66eb9c8f98d100a7017aaa8568e27213ff5443b"},{"sha":"0d1d53e15a6c60f75190b69a3826941636b2b9d4","author":{"email":"f282ad438ecadc93e62523946ab50d77b680b96f@epfl.ch","name":"Samuel Gruetter"},"message":"typ_has_total works (because wf_typ is strong enough)","distinct":true,"url":"https://api.github.com/repos/samuelgruetter/dot-calculus/commits/0d1d53e15a6c60f75190b69a3826941636b2b9d4"}]}