coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
2009-09-26	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-04-10	Fix tauto no longer failing after commit 12077; appropriate error	herbelin
2009-04-09	Turning tauto into a classical tautology prover as soon as classical	herbelin
2009-01-29	Solves some warning and hides some not-bad ones in doc. It remains a	herbelin
2008-12-30	- Fixed bugs and compatibilities issues in	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-25	More compatibility fixes, revert the tauto fix that prevented	msozeau
2008-07-24	Tauto breaking not only binary "conjunctions" seems like a bad idea	msozeau
2008-07-22	A try at allowing matching on applications as a binary syntax node by default.	msozeau
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-03-30	Modifications diverses et variées :	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2003-12-23	* empty log message *	barras
2003-11-12	petits changements de syntaxe	barras
2003-10-16	nouvelle syntaxe de ltac	barras
2003-09-22	Passage à la V8 par défaut	herbelin
2003-07-03	switching back to old tauto	corbinea
2003-07-02	added hints into Ground	corbinea
2003-06-27	* empty log message *	courant
2003-05-22	Preservation affichage des ?n en V7	herbelin
2003-05-21	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-31	Ajout d'un message à FailTac	herbelin
2003-03-28	Fixed Relative names not,iff in Camlp4 quotation.	corbinea
2003-03-18	Introducing Christine's Intuition1 and adding some invertible hyps.	corbinea
2003-02-26	Changed Tauto so it displays less 'Unfold not iff'	corbinea
2003-02-05	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea
2003-01-23	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-07-19	correction bugs Tauto	courant
2002-07-17	Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3\|- ?]	corbinea
2002-07-15	Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait	courant
2002-05-30	Nettoyage	herbelin
2002-05-29	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin
2002-05-22	Correction of a bug in Intuition (no more decomposition of dependent pairs).	corbinea
2002-05-15	Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de	herbelin
2002-05-15	Finalement VTactic est gardé pour y plonger les tactiques ML, le	herbelin
2002-05-14	- Changement de l'ordre de filtrage dans "Match Context"	herbelin
2002-05-02	nettoyage code	courant
2002-04-08	* empty log message *	courant
2002-03-21	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant