coq - The formal proof system

Age	Commit message (Expand)	Author
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
2002-03-20	Intuition now takes an (optional) tactic as parameter. This tactic is	courant
2002-03-15	Tauto est maintenant stable par "Intro" :	courant
2002-02-11	substitution et pattern modulo let	barras
2001-12-20	Mise en place de la réduction sous forme d'implications d'atomes en fn de tête	herbelin
2001-12-20	Utilisation de Hnf plutôt que Red	herbelin
2001-12-19	Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le Orelse	herbelin
2001-12-19	Insertion de Red sur chaque atome dans Tauto et Intuition	herbelin
2001-12-19	Tentative d'amélioration du résultat de Intuition	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-10-23	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye
2001-09-30	Ajout du printer de tactiques + modif du Dynamic ocaml	delahaye
2001-08-10	Parsing	herbelin
2001-08-08	Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme	courant
2001-06-25	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin
2001-06-15	Fix d'un bug de Tauto	delahaye
2001-06-01	Correction d'un bug du a un Intros trop violent	delahaye
2001-04-24	Ajout du cas True->A\|-B	delahaye