coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Simplifying the proof of NoRetractToModalProposition.paradox in	Hugo Herbelin	2017-02-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Hurkens.v by dropping the artificial need for monad laws. Tactic eauto decided to be dependent on the laws but there is a shorter proof without them. [Interestingly, eauto is not able to find the short proof. This is a situation of the form subgoal 1: H : ?A \|- P x subgoal 2: H : M ?A \|- M (forall x, P x) where addressing the second subgoal would find the right instance of ?A, but this instance is too hard to find by addressing first the first subgoal.]
*	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
\| \| \| \|	variables and definitions in sections is unsupported.
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
\| \| \| \| \| \|	The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet.
*	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
\| \| \| \| \| \| \| \| \|	Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
*	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
\| \| \|	Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
*	Hurkens.v: new paradox: type of modal propositions is not a retract.	Arnaud Spiwack	2014-09-26
\| \| \|	In particular there is no retract of the type of negative propositions in a negative proposition.
*	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
\| \| \| \|	Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.
*	Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing	herbelin	2012-11-15
\| \| \| \| \| \| \|	it as a consequence of the derivability of Hurkens' paradox in the presence of a retract from Type to Prop. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15977 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
\| \| \| \| \| \| \|	Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fixed various Overfull in documentation.	herbelin	2009-01-27
\| \| \| \| \| \| \| \| \| \|	- Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵	herbelin	2003-11-29
\| \| \| \| \| \|	par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rien de bien important	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4778 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Blancs	herbelin	2003-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3976 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v	herbelin	2002-05-29
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2712 85f007b7-540e-0410-9357-904b9bb8a0f7