coq - The formal proof system

Age	Commit message (Expand)	Author
2006-06-08	nouvelle MAJ	herbelin
2006-06-08	Changement du type d'argument 'TacticArgType X' en un type	herbelin
2006-06-08	MAJ coqc.byte et coqmktop.byte	herbelin
2006-06-08	Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...	notin
2006-06-08	Warning ocaml 3.09 pour variable inutile	herbelin
2006-06-08	Factorisation utilisation environnement dans make_pr_tac	herbelin
2006-06-08	reparation bug 1006	letouzey
2006-06-08	Correction du bug #728(1086) (ordre de sauvegarde des tactiques dans coqide)	notin
2006-06-08	DÃ©tection bug rawwit suitecorrection trou de typage create_arg	herbelin
2006-06-07	replace by	herbelin
2006-06-07	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin
2006-06-07	Ajout Whelp	herbelin
2006-06-07	petites corrections dans la doc de functional xxx.	courtieu
2006-06-07	Nouveaux Parametres Inductifs	cpaulin
2006-06-07	Réparation coqtop.ml	notin
2006-06-07	Changement de l'option -where: on vérifie si la variable d'environnement COQ...	notin
2006-06-07	functional induction can now be used with	jforest
2006-06-07	mise en texttt d'une commande.	courtieu
2006-06-07	Changements sur Functional xxx. Plus précis et plus exact.	courtieu
2006-06-06	Ajout de précisions dans la doc de functional scheme et consort +	courtieu
2006-06-06	this time it's good	jforest
2006-06-06	Error in last commit	jforest
2006-06-06	Debut modif parametres inductifs CIC	cpaulin
2006-06-06	protecting an uncaught exception Not_found	jforest
2006-06-06	reparation pour le bug #1072 (soufflee par J. Forest):	letouzey
2006-06-06	+ ameliorating the tactic "functional induction"	jforest
2006-06-05	Oh le joli bug dans le kernel:	letouzey
2006-06-05	Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext...	letouzey
2006-06-05	nouveaux parametres	cpaulin
2006-06-04	MAJ svn:ignore coqc.opt et coqmktop.opt	herbelin
2006-06-04	Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...	herbelin
2006-06-04	Ajout exists! et restructuration/extension des fichiers sur la	herbelin
2006-06-04	Ajout exists! et restructuration/extension des fichiers sur la	herbelin
2006-06-02	debut de reparation du test d'extraction	letouzey
2006-06-01	Update Program/subtac documentation.	msozeau
2006-06-01	Fix some nasty bug with the evars-to-dependent sum encoding.	msozeau
2006-06-01	bug in alpha-conversion	jforest
2006-06-01	reparation bug #1128	letouzey
2006-05-31	Fusion if.v et If.v (MacOS X ne sait pas distinguer la casse)	herbelin
2006-05-31	Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casse	herbelin
2006-05-31	ajout de QArith dans les theories standards	letouzey
2006-05-31	petits ajouts	letouzey
2006-05-31	Replacing the old version of "functional induction" with the new one.	jforest
2006-05-31	Colorisation dans Coqide	notin
2006-05-30	retour au comportement antérieur pour une application de foncteur:	letouzey
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-05-30	Correction bug #990 (LoadPath et option -R de coqide	notin
2006-05-30	* suite de la revision des wrappers Make	letouzey
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-05-29	Fix broken paths.	msozeau