coq - The formal proof system

Age	Commit message (Expand)	Author
2002-05-14	Utilisation d'une construction spéciale SECVAR pour gérer la	herbelin
2002-05-03	Simplification du filtrage si la premiere ligne de motifs est inevitable + au...	herbelin
2002-04-11	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin
2002-04-10	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin
2002-04-08	export de la fonction Reductionops.find_conclusion pour l'extraction	letouzey
2002-04-02	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras
2002-03-28	petite erreur dans le typage des let-in	barras
2002-03-26	Prise en compte des dependances dans la tactique Case	mohring
2002-03-21	Décomposition de l'application n-aire en application binaire pour que Patter...	herbelin
2002-03-04	Nouveau Rewrite-in plus economique	barras
2002-03-01	Nouveau comportement: Delta ne s'applique pas aux variables liées par un let	herbelin
2002-02-19	typage du produit: type_judgment appele avec contexte incorrect	barras
2002-02-19	meilleur message d'erreur lorsqu'on type une evar qui n'existe pas	barras
2002-02-19	Le type des evars transformees en meta n'etait pas normalise, et des Evars	barras
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