coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	"subst." works now even when it exists an hypothesis have the form "x=x" in t...	jforest	2006-05-20
*	suite tentative pour permettre l'utilisation de modules de FSets	letouzey	2006-05-20
*	on cache autant que possible Raw dans FSet(Weak)List.Make	letouzey	2006-05-19
*	tests de Romega	letouzey	2006-05-19
*	Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort	herbelin	2006-05-19
*	ajout de mes modifs recentes	letouzey	2006-05-18
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 85f007b7-540e-04...	letouzey	2006-05-18
*	Dépendances pour List.v	notin	2006-05-18
*	Correcting a bug in matching context on if.	jforest	2006-05-17
*	Typo dans List.v	notin	2006-05-17
*	updating Function documentation	jforest	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
*	Typo dans CREDITS	notin	2006-05-16
*	ajout de theories/FSets/DecidableTypeEx.v	letouzey	2006-05-15
*	3*rien	letouzey	2006-05-15
*	ajout d'exemples de decidable types	letouzey	2006-05-15
*	petit ajout concernant InA	letouzey	2006-05-15
*	On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_pos	letouzey	2006-05-14
*	In_dec de nouveau transparent	letouzey	2006-05-14
*	reparartion d'un petit oubli cassant PrecedenceGraph	letouzey	2006-05-14
*	typo	letouzey	2006-05-13
*	un Zgcd calculant dans coq	letouzey	2006-05-13
*	Code mort	herbelin	2006-05-13
*	Correction trou de typage des éliminations d'inductifs introduit dans commit...	herbelin	2006-05-13
*	correction bugs de condition de garde (fix + cofix)	barras	2006-05-12
*	une fonction pouvant calculer le gcd en coq	letouzey	2006-05-11
*	quelques ajouts venant des fichiers de Evelyne C.	letouzey	2006-05-11
*	decidabilite de InA	letouzey	2006-05-11
*	Comments about profiling	herbelin	2006-05-11
*	Oubli des symboles du Latin-1	herbelin	2006-05-11
*	Duplication du fichier FSetProperties pour les ensembles Weak.	letouzey	2006-05-11
*	r9089@thot: notin \| 2006-05-10 14:40:51 +0200	notin	2006-05-11
*	correction bugs dans Cbv (beta n-aire)	barras	2006-05-10
*	Conformité nouveaux principes: Declare Module non utilisable pour définir u...	herbelin	2006-05-10
*	Centralisation de la détection lettre/symbole par le lexeur dans les plages ...	herbelin	2006-05-10
*	subst. explicites avec vecteurs	barras	2006-05-09
*	Correcting an old bug during generation of generale recursive functions.	jforest	2006-05-09
*	+ correcting a bug in general recursive function (match e with _ => match f e...	jforest	2006-05-07
*	doc du in de match/with	barras	2006-05-05
*	Protection mode Debug On contre Ctrl-D	herbelin	2006-05-05
*	Correction in generate_graph (now handles fun _ => fix ....)	jforest	2006-05-05
*	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras	2006-05-05
*	Vieux bug de fin 2004 gardé pour mémoire	herbelin	2006-05-05
*	Correction comportement clause _ du match goal	herbelin	2006-05-05
*	un Zgcd general gardant trace des coefs	letouzey	2006-05-05
*	encore un correctif sur le rewrite H in setoid:	letouzey	2006-05-05
*	- intégration de la modification suggérée par L. Mamane: coqmktop passe ma...	notin	2006-05-04
*	Fixing two minor bugs in recdef and graph of function generation.	jforest	2006-05-03
*	fixed bug #804: removed useless reduction in fix guard checking	barras	2006-05-03