coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	La mise en forme normale du prédicat d'élimination était un peu trop viole...	herbelin	2001-11-22
*	Amélioration message Cases	herbelin	2001-11-21
*	Quelques autres petits problèmes résolus...	herbelin	2001-11-21
*	* empty log message *	herbelin	2001-11-21
*	MAJ	herbelin	2001-11-21
*	Amélioration messages d'erreur arité incorrecte (notamment record)	herbelin	2001-11-21
*	Possibilité d'appeler check avec l'option -byte	herbelin	2001-11-21
*	Simplification de la propagation du prédicat, bugs, et messages d'erreurs	herbelin	2001-11-21
*	documentation de mes actions recentes sur les theories (PL)	letouzey	2001-11-21
*	remise au gout du jour du repertoire theories/Sorting de la V6.3	letouzey	2001-11-21
*	remise au gout du jour du repertoire theories/Sorting de la V6.3	letouzey	2001-11-21
*	La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...	herbelin	2001-11-21
*	Solution partielle au problème des alias dépendants pour les rendre compati...	herbelin	2001-11-21
*	Prise en compte des '?' aussi dans le type des définitions	herbelin	2001-11-21
*	Oubli des contraintes d'univers lors de la suppression des cast dans un commi...	herbelin	2001-11-21
*	Make sure that NatRing won't loop forever.	bertot	2001-11-21
*	Un bug dans le script	herbelin	2001-11-21
*	Sur l'exahustivité du filtrage	herbelin	2001-11-21
*	Sur la cumulativité dans les tactiques	herbelin	2001-11-21
*	Nouveaux exemples	herbelin	2001-11-21
*	Prise en compte des coercions pour typer les branches lorsqu'il y a une contr...	herbelin	2001-11-21
*	Ajout isEvar	herbelin	2001-11-20
*	Ajout make_arity_signature	herbelin	2001-11-20
*	Ajout mkArity	herbelin	2001-11-20
*	hack temporaire concernant les remarks/modules	letouzey	2001-11-20
*	iota généralisé	letouzey	2001-11-20
*	* empty log message *	herbelin	2001-11-20
*	Correction bug contrainte de valeur trop restrictive sur le typage du type du...	herbelin	2001-11-20
*	types vs constr	herbelin	2001-11-20
*	Bug mauvaise instance	herbelin	2001-11-20
*	Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant	herbelin	2001-11-20
*	types vs constr	herbelin	2001-11-20
*	Cosmétique avant tout	herbelin	2001-11-20
*	Suppression des Cast externes dans les définitions	herbelin	2001-11-20
*	Code mort	herbelin	2001-11-20
*	Ajout quelques fonctions; code mort	herbelin	2001-11-20
*	Bug nommage des fonctions définies par récursion mutuelle	herbelin	2001-11-19
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Mise en place d'une méthode directe pour indiquer le type des déclarations ...	herbelin	2001-11-19
*	Re-installation de l'affichage des globaux par des noms courts	herbelin	2001-11-19
*	Renommage qualid_of_global en shortest_qualid_of_global	herbelin	2001-11-19
*	Re-installation de l'affichage des globaux par des noms courts	herbelin	2001-11-19
*	Remise en place du Cast pour Correctness	herbelin	2001-11-19
*	User Casts are for helping pretyping, experimentally not to be kept	herbelin	2001-11-17
*	MAJ	herbelin	2001-11-16
*	* empty log message *	herbelin	2001-11-16
*	Ajout d'un fichier Max dans Arith, et enrichissement du Min.	letouzey	2001-11-15
*	Ajout des fonctions tail-recursives tail_plus et tail_mult.	letouzey	2001-11-15
*	Une liste plus precise des .v a prendre en compte pour les dependances, a l'e...	herbelin	2001-11-14
*	oubli: changement de nil en nilT	mayero	2001-11-14