coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	sed s'/_one_var/_on/g'	Jason Gross	2014-08-26
*	Generalize EqdepFacts	Jason Gross	2014-08-26
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Generalize eq_proofs_unicity	Jason Gross	2013-12-12
*	Improved the presentation of the proof of UIP_refl_nat.	Hugo Herbelin	2013-12-04
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Identities over types satisfying Uniqueness of Identity Proofs	herbelin	2012-12-04
*	For the record, two examples of short proofs of uniqueness of identity	herbelin	2012-11-15
*	Updating headers.	herbelin	2012-08-08
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added UIP_dec on suggestion of Eelis on #coq irc.	herbelin	2010-05-22
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	added a lemma to prove inj_pair2 when eq_dec is available.	vsiles	2007-09-26
*	Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc,	notin	2007-06-21
*	Passage de Set à Type dans Relations et Wellfounded	herbelin	2007-02-06
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
*	Mise en forme des theories	notin	2006-10-17
*	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin	2006-03-05
*	Nouvelle en-tête	herbelin	2004-07-16
*	simplified proof (eq and eqT are now the same)	barras	2004-06-25
*	eq2eqT et eqT2eq devenus obsolètes	herbelin	2004-06-02
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)	barras	2001-06-18
*	Mise de (*i autour CVS info	mohring	2001-04-19
*	documentation automatique de la bibliothèque standard	filliatr	2001-04-11
*	entetes	filliatr	2001-03-15
*	Renommage des variables dans les schémas d'induction	herbelin	2001-02-14
*	caractere opaque des constantes repris en compte	filliatr	2000-12-04
*	Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...	herbelin	2000-03-21
*	Syntactic Definition n'etaient pas correctemenet importees	filliatr	2000-03-16
*	* empty log message *	barras	2000-03-10
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21