coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prise en compte des variables de grammaires de tactiques et dédollarisation ...	herbelin	2003-04-08
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	code mort	herbelin	2003-04-07
*	Backtrack du commit de Christine, qui posait probleme avec FTC	letouzey	2003-04-03
*	Extension de Replace aux égalités entre preuves	herbelin	2003-04-01
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Ajout d'un message à FailTac; localisation des appels à des tactiques défi...	herbelin	2003-03-31
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
*	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
*	* empty log message *	barras	2003-03-12
*	Changed Tauto so it displays less 'Unfold not iff'	corbinea	2003-02-26
*	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-13
*	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea	2003-02-05
*	Un type "standardisé" pour new_hyp	herbelin	2003-01-25
*	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea	2003-01-23
*	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-22
*	Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur	herbelin	2003-01-21
*	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-20
*	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-19
*	Subst sur une hyp qui n'existe pas ne fait pas une anomalie	barras	2003-01-16
*	correction de bug de Subst: ne faisait rien lorsque l'hypothese	barras	2003-01-09
*	Commentaires; optimisation	herbelin	2002-12-30
*	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin	2002-12-24
*	code mort	herbelin	2002-12-24
*	Re-essai de forcer le terme réécrit à apparaître dans le but	herbelin	2002-12-23
*	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-21
*	suite du commit precedent	barras	2002-12-19
*	nouveau Subst:	barras	2002-12-17
*	Traitement spécial pour les types à l'internalisation	herbelin	2002-12-15
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)	herbelin	2002-12-10
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	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-14
*	Raffinement de l'heuristique d'unification dans sig_clausale_forme	herbelin	2002-11-06
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local	herbelin	2002-10-23