coq - The formal proof system

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