aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/Hurkens.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Simplifying the proof of NoRetractToModalProposition.paradox inGravatar Hugo Herbelin2017-02-24
* Fix a typo in Hurkens.v commentGravatar Jason Gross2016-12-19
* Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* Hurkens.v: Fix a syntax error.Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: new paradox: type of modal propositions is not a retract.Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: fix coqdoc formatting in a comment.Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: update comments.Gravatar Arnaud Spiwack2014-09-25
* Hurkens.v: show proofs in coqdoc.Gravatar Arnaud Spiwack2014-09-24
* Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].Gravatar Arnaud Spiwack2014-09-24
* Hurkens.v: coqdoc documentation.Gravatar Arnaud Spiwack2014-09-24
* A new version of Hurkens.v.Gravatar Arnaud Spiwack2014-09-24
* Isolating the ingredients of the proof of Prop<>Type (r15973). SeeingGravatar herbelin2012-11-15
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Rien de bien importantGravatar herbelin2003-11-02
* BlancsGravatar herbelin2003-04-29
* Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vGravatar herbelin2002-05-29