coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix name clash in "failure/inductive.v".	xclerc	2013-09-20
*	Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.	xclerc	2013-09-20
*	Merge "inductive?.v" tests into a single "inductive.v" test.	xclerc	2013-09-20
*	Use "Fail" rather than rely on exit code.	xclerc	2013-09-20
*	Uminus.v : prepare this test file for the use of Fail	letouzey	2013-09-19
*	universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes	letouzey	2013-09-19
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Updating headers.	herbelin	2012-08-08
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Fixing critical inductive polymorphism bug found by Bruno.	herbelin	2011-10-05
*	Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v	herbelin	2011-04-08
*	Fix inconsistency in Prop/Set conversion check	glondu	2010-09-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added examples for checking that the guard condition excludes subterms	herbelin	2010-05-20
*	Fixed bug #2260 (check of resolution of all evars in the declaration	herbelin	2010-03-24
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	Fixed a bug introduced in revision 12265.	herbelin	2009-10-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin	2009-08-11
*	fixed kernel bug (de Bruijn) + test-suite	barras	2008-12-02
*	added tests for hyps reordering	barras	2008-11-27
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	fixed universes bug related to module inclusion	barras	2008-04-22
*	test module include w.r.t. universe constraints	barras	2008-04-21
*	Vérification que "rewrite in" se comporte comme "rewrite" et échoue	herbelin	2007-10-16
*	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin	2007-09-06
*	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran	2007-02-21
*	Tests de référence circulaire au sous-typage de module (pour mémoire)	herbelin	2007-01-19
*	Correction bug #1302	herbelin	2007-01-17
*	test condition de garde	barras	2006-12-13
*	Check that sort-polymorphic inductive types is not too lax	herbelin	2006-10-27
*	Cette dérivation de paradoxe passait en V8.1beta	herbelin	2006-10-27
*	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin	2006-10-13
*	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest	2006-08-22
*	Stricte positivité en présence de types inductifs imbriqués avec paramètr...	herbelin	2006-06-23
*	Deux vérifications que le polymorphisme de sorte des inductifs ne fonctionne...	herbelin	2006-06-22
*	Correction trou de typage des éliminations d'inductifs introduit dans commit...	herbelin	2006-05-13
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	cf ltac4.v	herbelin	2005-12-21
*	deplacement params_ind	mohring	2005-11-03
*	test-suite/output/Notations.out	herbelin	2004-11-17
*	* empty log message *	herbelin	2004-10-17
*	Nouvelle en-tête	herbelin	2004-07-16
*	ajout test de non-regression Clear d'une def locale	barras	2003-12-17
*	Cacher les .v8	herbelin	2003-10-10
*	test d'implicite incorrect depuis que eq porte sur Type	barras	2003-09-23
*	* empty log message *	herbelin	2003-01-20
*	Tests ltac	herbelin	2003-01-19