coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Correction d'une incompatibilité de nommage introduite lors du commit préc�...	herbelin	2002-10-22
*	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin	2002-10-21
*	NewDestruct/NewInduction acceptent l'option "using"	herbelin	2002-10-21
*	L'application de ltac attend une référence; meilleure protection contre	herbelin	2002-10-14
*	Réparation bug Inversion (#212)	herbelin	2002-10-14
*	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras	2002-10-09
*	Subst ne fait pas clear sur x:=e	filliatr	2002-10-08
*	Oops...	coq	2002-10-01
*	Table fonctionnelle dans autorewrite	coq	2002-10-01
*	Vraie substitutivite de autohints	coq	2002-10-01
*	bug de noms long pour eqT.	clrenard	2002-10-01
*	Que des niveaux d'univers frais dans le type des constantes globales	herbelin	2002-09-29
*	passage a ocaml 3.06	herbelin	2002-09-27
*	Subst (tout court)	filliatr	2002-09-16
*	tactique Subst x1 ... xn	filliatr	2002-09-11
*	Code mort de AutoRewrite	herbelin	2002-09-09
*	correction de bugs:	barras	2002-08-16