coq - The formal proof system

Age	Commit message (Expand)	Author
2003-02-27	MAJ	herbelin
2003-02-27	Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'...	herbelin
2003-02-27	Correction test token normal	herbelin
2003-02-27	1.342 par rapport a 1.340 contourne un bug '-pp camlp4o' (version 1.341 corro...	herbelin
2003-02-27	Contournement bug '-pp camlp4o'	herbelin
2003-02-27	Le lexeur et Notation savent reconnaître si un unicode des blocs	herbelin
2003-02-27	Adding tests for the "functional induction" facility.	bertot
2003-02-27	The contribution of Pierre Courtieu on generating specialized induction schemes	bertot
2003-02-27	Retour nouvel afficheur	herbelin
2003-02-27	Restructuration des hints pour qu'Auto fasse moins de détours et les	herbelin
2003-02-27	maj	filliatr
2003-02-26	Changed Tauto so it displays less 'Unfold not iff'	corbinea
2003-02-26	coqide: preliminary support for mnemonics. Edit menu. Context help now works ...	monate
2003-02-26	maj	filliatr
2003-02-25	ide:copy/paste fix	monate
2003-02-25	Suppression des warnings a la compilation de contrib/linear	corbinea
2003-02-25	maj	filliatr
2003-02-24	coqide : aide sur selection ou sur mot	monate
2003-02-24	Bringing Linear back to life (Still somewhat buggy).	corbinea
2003-02-24	aide contextuelle / menus compilation + print + export	filliatr
2003-02-24	on sait se refaire uniquement si option -f	filliatr
2003-02-24	coq_makefile dit comment faire le .depend (evite l'echec lorsque	filliatr
2003-02-24	False dependencies in summary	coq
2003-02-24	ide changes	monate
2003-02-24	ctrl-k like Emacs in coqide	monate
2003-02-24	ide	monate
2003-02-24	* empty log message *	monate
2003-02-22	maj	filliatr
2003-02-21	CoqIDE: robustesse / multi-buffers / menus / ... (utilisable)	filliatr
2003-02-21	bugs/améliorations trouvés via FTA	letouzey
2003-02-17	Affinement entree annot	herbelin
2003-02-15	maj	filliatr
2003-02-14	prise en compte des sous-repertoires Coq de maniere dynamique	filliatr
2003-02-14	Ajout du theoreme de Cesaro	desmettr
2003-02-14	MAJ pour Reals/SeqSeries.v	desmettr
2003-02-13	Test de non bouclage malencontreux dans les niveaux	herbelin
2003-02-13	Modifications dans une tactique toplevel	delahaye
2003-02-13	Correction d'un bug introduit dans le backtracking d'occurrence	delahaye
2003-02-13	Chargement dynamique de .cma	delahaye
2003-02-13	Debugger plus informatif	delahaye
2003-02-12	maj	filliatr
2003-02-11	Undo dans Coq IDE	filliatr
2003-02-08	Bug Rename	herbelin
2003-02-08	Bug Rename	herbelin
2003-02-06	MAJ	herbelin
2003-02-06	commentaire	coq
2003-02-06	maj	filliatr
2003-02-05	update	desmettr
2003-02-05	Ajout du traducteur	desmettr
2003-02-05	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea