coq - The formal proof system

Age	Commit message (Expand)	Author
2003-03-29	eq fusionne avec eqT et devient par défaut sur Type,	herbelin
2003-03-28	notations <>, Assumption avec existentiel, replace term	mohring
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-03-12	* empty log message *	barras
2003-02-26	Changed Tauto so it displays less 'Unfold not iff'	corbinea
2003-02-13	Correction d'un bug introduit dans le backtracking d'occurrence	delahaye
2003-02-13	Chargement dynamique de .cma	delahaye
2003-02-13	Debugger plus informatif	delahaye
2003-02-05	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea
2003-01-25	Un type "standardisé" pour new_hyp	herbelin
2003-01-23	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea
2003-01-22	Mauvais environnement d'évaluation pour les globaux	herbelin
2003-01-22	Correction bug réecriture à la racine pour le sétoide Prop.	clrenard
2003-01-21	Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur	herbelin
2003-01-20	Mauvaise interprétatin de IdentArgType	herbelin
2003-01-20	Protection contre les noms de tactiques inconnus; restriction exceptions ratt...	herbelin
2003-01-20	Petits bugs	herbelin
2003-01-19	Utilisation d'une exception 'catchable'	herbelin
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin
2003-01-16	Subst sur une hyp qui n'existe pas ne fait pas une anomalie	barras
2003-01-09	correction de bug de Subst: ne faisait rien lorsque l'hypothese	barras
2002-12-30	Commentaires; optimisation	herbelin
2002-12-24	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin
2002-12-24	code mort	herbelin
2002-12-23	Re-essai de forcer le terme réécrit à apparaître dans le but	herbelin
2002-12-21	Backtrack sur la tentative d'interdire les K-abstractions dans l'unification	herbelin
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-19	suite du commit precedent	barras
2002-12-17	nouveau Subst:	barras
2002-12-15	Traitement spécial pour les types à l'internalisation	herbelin
2002-12-12	Ajout du vernac Proof with	gregoire
2002-12-10	Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)	herbelin
2002-12-09	Option pour rendre les vérifications du refiner optionnelle	herbelin
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-11-14	Re-ajout constrIn	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-14	JMeq now treated as an equality by tactics.	courant
2002-11-06	Raffinement de l'heuristique d'unification dans sig_clausale_forme	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-10-23	Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local	herbelin
2002-10-22	Correction d'une incompatibilité de nommage introduite lors du commit préc�...	herbelin
2002-10-21	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin
2002-10-21	NewDestruct/NewInduction acceptent l'option "using"	herbelin
2002-10-14	L'application de ltac attend une référence; meilleure protection contre	herbelin
2002-10-14	Réparation bug Inversion (#212)	herbelin
2002-10-09	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras
2002-10-08	Subst ne fait pas clear sur x:=e	filliatr
2002-10-01	Oops...	coq