coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	* empty log message *	courant	2003-01-31
*	Bug 'with Module' corrige	coq	2003-01-22
*	id_of_msid en plus	letouzey	2003-01-22
*	- amelioration des messages d'erreur de la condition de garde	barras	2002-12-18
*	Contexte locale non-vide interdit a la fin d'un module ou module type	coq	2002-12-18
*	Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse la	herbelin	2002-12-10
*	Déplacement du hash-consing vers declare.ml	herbelin	2002-12-10
*	Corrections de gestion des univers et modules + meilleure gestions des noms...	coq	2002-12-09
*	des Set et des Map en plus	letouzey	2002-12-05
*	suppression du champ mind_singl inutilisé dans mutual_inductive_body	letouzey	2002-12-04
*	Corrige un bug de composition de substitutions	coq	2002-12-04
*	Allègement du noyau	herbelin	2002-11-18
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	pattern-matching avec cas inutilise dans closure	barras	2002-10-15
*	Une fonction de moins dans .mli	coq	2002-10-07
*	Lazy manuelles dans le code	coq	2002-10-07
*	Lazy experimentale temporaire...	coq	2002-10-05
*	Comparaisons des types pendant le sous-typage reactive	coq	2002-09-30
*	Activation du hash-consing	herbelin	2002-09-29
*	Hash-consing pour kernel_name	herbelin	2002-09-29
*	Réparation hash_consing	herbelin	2002-09-29
*	La notation with dependante + affichage dependante de moduels corrige	coq	2002-09-20
*	La notation 'with'. L'interpretation - version preliminaire	coq	2002-08-19
*	Pretty-printing preliminaire des modules, commandes	coq	2002-08-19
*	Strengthenning rules for modules + No modules in sections	coq	2002-08-16
*	Renoncement	herbelin	2002-08-13
*	Petites corrections ici et la	coq	2002-08-13
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	resolution du pb d'efficacite du a Sign.add_named_decl	barras	2002-04-04
*	renommage de l'exception locale Arity	barras	2002-04-03
*	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras	2002-04-02
*	* empty log message *	mohring	2002-03-29
*	petite erreur dans le typage des let-in	barras	2002-03-28
*	code redondant	herbelin	2002-03-22
*	open Univ inutile	courant	2002-03-12
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
*	suppression de pop_named	barras	2002-02-22
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
*	substitution et pattern modulo let	barras	2002-02-11
*	erreur mineure dans le test des inductifs imbriques	barras	2002-02-07
*	petit nettoyage de kernel/inductive	barras	2002-02-07
*	evaluable_constant retournait vrai pour les constantes opaques, ce qui faisait	barras	2002-02-05
*	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring	2002-01-31
*	cosmetique	herbelin	2002-01-30
*	Reparation erreur de syntaxe	mohring	2002-01-30
*	modification de la definition des def inductives unitaires et autorisation d'...	mohring	2002-01-29
*	condition de positivite moins stricte vis-a-vis des parametres (cf bug de Edu...	barras	2002-01-29
*	Cas LetIn superflu dans check_construct car normalisation préalable	herbelin	2002-01-24