coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Simplifying the proof of NoRetractToModalProposition.paradox in	Hugo Herbelin	2017-02-24
*	Fix a typo in Hurkens.v comment	Jason Gross	2016-12-19
*	Fix bug #4503: mixing universe polymorphic and monomorphic	Matthieu Sozeau	2016-01-23
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
*	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
*	Update headers.	Maxime Dénès	2015-01-12
*	Fix some typos.	Guillaume Melquiond	2014-10-27
*	Fix some typos in comments.	Guillaume Melquiond	2014-10-27
*	Hurkens.v: Fix a syntax error.	Arnaud Spiwack	2014-09-26
*	Hurkens.v: new paradox: type of modal propositions is not a retract.	Arnaud Spiwack	2014-09-26
*	Hurkens.v: fix coqdoc formatting in a comment.	Arnaud Spiwack	2014-09-26
*	Hurkens.v: update comments.	Arnaud Spiwack	2014-09-25
*	Hurkens.v: show proofs in coqdoc.	Arnaud Spiwack	2014-09-24
*	Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].	Arnaud Spiwack	2014-09-24
*	Hurkens.v: coqdoc documentation.	Arnaud Spiwack	2014-09-24
*	A new version of Hurkens.v.	Arnaud Spiwack	2014-09-24
*	Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing	herbelin	2012-11-15
*	Updating headers.	herbelin	2012-08-08
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	- Fixed various Overfull in documentation.	herbelin	2009-01-27
*	Nouvelle en-tête	herbelin	2004-07-16
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Rien de bien important	herbelin	2003-11-02
*	Blancs	herbelin	2003-04-29
*	Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v	herbelin	2002-05-29