GitHub PushEvent at 2014-09-26 13:00:22
Repository: coq
Actor: letouzey
Payload: {"shas":[["48ba4c55159d0d9f9b13cfe82617ac4a68867885","1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","Hurkens.v: fix coqdoc formatting in a comment.","Arnaud Spiwack",true],["c74a70a73b3bf39394c551f1cdb224450bf77176","1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","Hurkens.v: new paradox: type of modal propositions is not a retract.\n\nIn particular there is no retract of the type of negative propositions in a negative proposition.","Arnaud Spiwack",true],["0a42f8d2434d6c5471d47c99d815762783cdca95","1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","ClassicalFacts: adds a proof that weak excluded middle implies weak proof irrelevance.\n\nApplication of previous commit in Hurkens.v.","Arnaud Spiwack",true]],"size":3,"ref":"refs/heads/trunk","head":"0a42f8d2434d6c5471d47c99d815762783cdca95"}