coq - The formal proof system

Age	Commit message (Expand)	Author
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
2006-05-09	Correcting an old bug during generation of generale recursive functions.	jforest
2006-05-07	+ correcting a bug in general recursive function (match e with _ => match f e...	jforest
2006-05-05	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-04	- intégration de la modification suggérée par L. Mamane: coqmktop passe ma...	notin
2006-05-03	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	bug #1096: whd_stack on one arg of conversion had side-effect on the other arg	barras
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-05-02	Changement de comportement de rewrite: face a une egalité setoid, on	letouzey
2006-05-02	Correction bug du correctif bug assert as	herbelin
2006-05-02	Option --coqlib_path pour coqdoc (suite et fin)	notin
2006-05-02	Affichage des warning gtk comme warning coq	herbelin
2006-05-02	Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ...	notin
2006-05-02	Bug assert as	herbelin
2006-04-29	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey
2006-04-29	meilleur nommage pour PairOrderedType	letouzey
2006-04-29	qq proprietes de plus sur Ncompare	letouzey
2006-04-28	Continue l'écriture de la doc de "Function". Pas fini, manque:	courtieu
2006-04-28	If function creates proof obligation, there are now printed once.	courtieu
2006-04-28	r8931@thot: notin \| 2006-04-28 16:19:38 +0200	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8767 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8766 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8765 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8764 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8763 85f007b7-540e-04...	notin