coq - The formal proof system

Age	Commit message (Expand)	Author
2002-02-18	bug #134: on appelait solve_simple_eqn avec une evar qui etait resolue	barras
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2002-02-14	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras
2002-02-12	petite modif pour ne pas expanser trop de let pendant l'unification	barras
2002-02-11	substitution et pattern modulo let	barras
2002-02-07	petit nettoyage de kernel/inductive	barras
2002-02-04	exceptionmal ratrappee	barras
2002-01-31	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring
2002-01-25	Correction bug 'Check [b]if b then O else O'	herbelin
2002-01-24	code mort	herbelin
2002-01-24	Réparation bug 'known_dependent'	herbelin
2002-01-21	warning en mode verbeux seulement	filliatr
2002-01-18	Le chargement des coercions est nécessaire même si le module n'est pas ouvert	herbelin
2002-01-17	Amélioration affichage échec lookup_eliminator	herbelin
2002-01-16	Correction d'un problème avec les motifs anonymes dépendant dans des argume...	herbelin
2002-01-15	Correction de de Bruijn incorrect pour le cas de dépendances vers l'avant	herbelin
2001-12-20	Non dépliage des Fix non réductibles dans Hnf	herbelin
2001-12-19	Insertion unification non seulement en tête mais à l'intérieur des motifs ...	herbelin
2001-12-18	Grossière erreur de typage	herbelin
2001-12-18	Nettoyage exceptions liées au vieux Case	herbelin
2001-12-18	Nettoyage exceptions liées au vieux Case; réparation du try with UserError ...	herbelin
2001-12-13	Contournement du problème des evars de type, typées par défaut dans Type (...	herbelin
2001-12-13	Contournement du problème des evars de type, typées par défaut dans Type	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-12-11	Mise en place de coercion dans les motifs	herbelin
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-22	La mise en forme normale du prédicat d'élimination était un peu trop viole...	herbelin
2001-11-21	Quelques autres petits problèmes résolus...	herbelin
2001-11-21	Simplification de la propagation du prédicat, bugs, et messages d'erreurs	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 coercions pour typer les branches lorsqu'il y a une contr...	herbelin
2001-11-20	Ajout make_arity_signature	herbelin
2001-11-20	Correction bug contrainte de valeur trop restrictive sur le typage du type du...	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-19	Bug nommage des fonctions définies par récursion mutuelle	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-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-09	Nettoyage coercions et classes	herbelin
2001-11-09	code mort	herbelin
2001-11-08	Introduction d'univers frais dans les types implicites engendrés par le pré...	herbelin
2001-11-08	Rétablissement de la persistance des Cast; typage des LetIn sans recours à ...	herbelin
2001-11-06	corrections mineures suite au commit de restructuration du noyau	barras
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-30	Reorganisation de Goption. Passage des options l'utilisant en synchrone	letouzey
2001-10-29	Amérioration message d'erreur en cas d'échec du filtrage de premier ordre	herbelin
2001-10-16	Nettoyage Recordobj et conséquences	herbelin