coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	* empty log message *	barras	2003-12-23
*	petits changements de syntaxe	barras	2003-11-12
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	Passage à la V8 par défaut	herbelin	2003-09-22
*	switching back to old tauto	corbinea	2003-07-03
*	added hints into Ground	corbinea	2003-07-02
*	* empty log message *	courant	2003-06-27
*	Preservation affichage des ?n en V7	herbelin	2003-05-22
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Fixed Relative names not,iff in Camlp4 quotation.	corbinea	2003-03-28
*	Introducing Christine's Intuition1 and adding some invertible hyps.	corbinea	2003-03-18
*	Changed Tauto so it displays less 'Unfold not iff'	corbinea	2003-02-26
*	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea	2003-02-05
*	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea	2003-01-23
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	correction bugs Tauto	courant	2002-07-19
*	Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3\|- ?]	corbinea	2002-07-17
*	Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait	courant	2002-07-15
*	Nettoyage	herbelin	2002-05-30
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29
*	Correction of a bug in Intuition (no more decomposition of dependent pairs).	corbinea	2002-05-22
*	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-15
*	- Changement de l'ordre de filtrage dans "Match Context"	herbelin	2002-05-14
*	nettoyage code	courant	2002-05-02
*	* empty log message *	courant	2002-04-08
*	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant	2002-03-21
*	Intuition now takes an (optional) tactic as parameter. This tactic is	courant	2002-03-20
*	Tauto est maintenant stable par "Intro" :	courant	2002-03-15
*	substitution et pattern modulo let	barras	2002-02-11
*	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-20
*	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-19
*	compat ocaml 3.03	filliatr	2001-12-13
*	Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR	delahaye	2001-10-23
*	Ajout du printer de tactiques + modif du Dynamic ocaml	delahaye	2001-09-30
*	Parsing	herbelin	2001-08-10
*	Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme	courant	2001-08-08
*	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin	2001-06-25
*	Fix d'un bug de Tauto	delahaye	2001-06-15
*	Correction d'un bug du a un Intros trop violent	delahaye	2001-06-01
*	Ajout du cas True->A\|-B	delahaye	2001-04-24
*	entetes	filliatr	2001-03-15
*	Ajout d'une heuristique pour les types dependants	delahaye	2001-02-05