coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Bug 2589: Documentation patch of Hendrik Tews	pboutill	2011-09-02
*	A module out of Program to have list notations (bug 2463)	pboutill	2011-04-08
*	Cosmetic : let's take advantage of the n-ary exists notation	letouzey	2010-12-17
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin	2010-07-22
*	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin	2010-07-18
*	Tentative de suppression de l'import automatique des hints et coercions.	herbelin	2010-07-18
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Granting wish #2229 (InA_dec transparent) and Michael Day's coq-club	herbelin	2010-04-10
*	Arith's min and max placed in Peano (+basic specs max_l and co)	letouzey	2010-02-17
*	Addition of mergesort + cleaning of the Sorting library	herbelin	2009-12-13
*	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin	2009-11-11
*	List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...	letouzey	2009-11-02
*	Remove various useless {struct} annotations	letouzey	2009-11-02
*	list, length, app are migrated from List to Datatypes	letouzey	2009-11-02
*	Fix flat_map definition so that it plays nicely with fix	glondu	2009-10-29
*	MSets: a new generation of FSets	letouzey	2009-10-13
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	adds a property on map	bertot	2009-08-19
*	adds lemmas on interactions between existsb, forallb, and app	bertot	2009-08-19
*	- Add more precise error localisation when one of the application fails	herbelin	2009-08-04
*	List: add a iff-based lemma about In and ++	letouzey	2009-07-24
*	Very-small-step policy changes to the library.	herbelin	2009-06-06
*	Add lemmas on lists: nth_default_eq, map_nth_error	glondu	2008-08-06
*	Cyclic31: migrate auxiliary lemmas to their legitimate files	letouzey	2008-05-27
*	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin	2008-05-09
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau	2008-04-28
*	- Fix bug in unification not taking into account the right meta	msozeau	2008-04-27
*	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau	2008-04-08
*	Correction du bug #1819	notin	2008-04-01
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey	2007-11-06
*	two additionnal results on list append (coming from theories/ints/List/ListAu...	letouzey	2007-11-01
*	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin	2006-10-26
*	Indentation + typo	notin	2006-09-01
*	Argument Scope de list déplacé dans List.v	herbelin	2006-07-09
*	Quelques Hint inutiles	herbelin	2006-07-06
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	Typo dans List.v	notin	2006-05-17
*	Ajout de [count_occ] dans List.v	notin	2006-05-17
*	etoffage des notions de permutations (a la fois List.Permutation et Permutati...	letouzey	2006-05-16
*	In_dec de nouveau transparent	letouzey	2006-05-14
*	r9089@thot: notin \| 2006-05-10 14:40:51 +0200	notin	2006-05-11
*	versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes	letouzey	2006-04-06
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	In_dec transparent (wish #902)	herbelin	2004-12-19
*	Nouvelle en-tête	herbelin	2004-07-16
*	Ajout delimiteur et arguments de scope pour list	herbelin	2003-12-24
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29