coq - The formal proof system

Age	Commit message (Expand)	Author
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-20	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-19	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-17	User Casts are for helping pretyping, experimentally not to be kept	herbelin
2001-11-16	MAJ	herbelin
2001-11-16	* empty log message *	herbelin
2001-11-15	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-14	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	Changement de list en listT, cons en consT et app en appT	mayero
2001-11-14	Suppression d'Export redondants	herbelin
2001-11-14	Revolution culturelle: suppression des arguments prop	letouzey
2001-11-13	Moins de fichiers avec des axioms	letouzey
2001-11-12	suppression d'axiomes dans Rstar, Newman et Integers	letouzey
2001-11-12	Suppression des stamps et donc des *_constraints	clrenard
2001-11-12	suite du petit oups	letouzey
2001-11-12	petit oups	letouzey
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-12	suite refonte extraction.ml	letouzey
2001-11-12	Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)	letouzey
2001-11-09	MAJ après restructuration kernel	herbelin
2001-11-09	Nettoyage coercions et classes	herbelin
2001-11-09	Déplacement et export de type_of_global dans Global	herbelin
2001-11-09	MAJ pour make doc	herbelin
2001-11-09	code mort	herbelin
2001-11-09	typo	letouzey