coq - The formal proof system

Age	Commit message (Expand)	Author
2006-05-23	Clarification role de library_part : renommage en remove_section_part	herbelin
2006-05-23	cleanning code	jforest
2006-05-23	PÃrÃ©ouverture de la plupart des fichis pour Ã©viter d'avoir Ã qualifier	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-05-22	un debut de propriétés concernant FMap	letouzey
2006-05-22	suite des marquages de types et opacifications de lemmes dans les wrappers Make	letouzey
2006-05-22	Correcting a bug in identifiers manipulation	jforest
2006-05-22	LetTuple are now supported in Function	jforest
2006-05-22	Modification de l'appel à coqdoc (COQBIN)	notin
2006-05-22	encore un exemple ne marchant pas, ni avec omega ni avec romega	letouzey
2006-05-22	MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...	herbelin
2006-05-22	MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...	herbelin
2006-05-20	auto with zarith genere des sous-lemmes silencieusement,	letouzey
2006-05-20	"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-19	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-18	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-17	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-16	etoffage des notions de permutations (a la fois List.Permutation et Permutati...	letouzey
2006-05-16	Typo dans CREDITS	notin
2006-05-15	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-14	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-13	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-12	correction bugs de condition de garde (fix + cofix)	barras
2006-05-11	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-10	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-09	subst. explicites avec vecteurs	barras