coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Message d'erreur plus explicite pour Tauto	delahaye	2001-02-05
*	rétablissement nouveau Tauto	filliatr	2001-02-05
*	Résolution d'un bug de simplification	delahaye	2001-02-03
*	oubli de Closure.EvalConstRef	filliatr	2001-02-01
*	- coqc : option -image	filliatr	2001-02-01
*	Bug fixed: the case [ id : ?1 -> ?2 \|- ?] was missing in tauto_main	sacerdot	2001-01-30
*	As an heuristic, now both in tauto and intuition we try to avoid the initial	sacerdot	2001-01-29
*	Elimination du '	delahaye	2000-11-28
*	Nouveau choix pour l'intros initial	delahaye	2000-11-24
*	On n'introduit que des produits non dependants	delahaye	2000-11-23
*	compilation des fichiers ml4 sans GNUseries	filliatr	2000-11-03
*	Remplacement de Tauto et Intuition	delahaye	2000-10-30