coq - The formal proof system

Age	Commit message (Expand)	Author
2002-07-16	un cas inutile dans un pattern matching	letouzey
2002-07-02	reparation pretyping ROldCase dans le cas let	filliatr
2002-07-02	factorisation code dans make_dep_of_undep	filliatr
2002-06-26	* empty log message *	mohring
2002-06-26	* empty log message *	mohring
2002-06-13	Nouvelle version de l'algorithme de compilation du filtrage compatible avec u...	herbelin
2002-06-13	Ajout map_inductive_type et map_ind_family	herbelin
2002-06-07	L'ordre supérieur avait quelque peu été oublié dans l'unification...	herbelin
2002-05-30	Mise au point de declare_red_expr	herbelin
2002-05-30	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
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