coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	AutoRewrite substitutive...	coq	2002-08-13
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Branchement de Assert, Pose et LetTac sur l'algo de création de noms	herbelin	2002-07-30
*	correction bugs Tauto	courant	2002-07-19
*	tactique Subst	filliatr	2002-07-17
*	Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3\|- ?]	corbinea	2002-07-17
*	Bug dans la globalisation des arguments de tactiques primitives	herbelin	2002-07-16
*	Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait	courant	2002-07-15
*	Que la localisation des erreurs pour les tactiques atomiques marche	herbelin	2002-07-11
*	Hack pour autoriser les $n dans les Grammar tactic	herbelin	2002-07-03
*	Réparation de l'interprétation des fermetures (sans casser Field!)	herbelin	2002-06-13
*	Ajout coercion constr vers hyp quantifiée	herbelin	2002-06-06
*	Tentative de réparation d'un bug Omega: une variable de section qui après e...	herbelin	2002-06-06
*	Passage de PatternMatchingFailure vers UserError pour capture par tclFIRST	herbelin	2002-06-06
*	Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...	herbelin	2002-06-05
*	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...	herbelin	2002-06-05
*	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...	herbelin	2002-06-05
*	Les VContext ne sont plus des fermetures (temporaire)	delahaye	2002-05-31
*	Nettoyage	herbelin	2002-05-30
*	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin	2002-05-30
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Réorganisation des tclTHEN (cf dev/changements.txt)	herbelin	2002-05-29
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29
*	Pour les tactiques dépendant de False	herbelin	2002-05-29
*	Correction of a bug in Intuition (no more decomposition of dependent pairs).	corbinea	2002-05-22