coq - The formal proof system

Age	Commit message (Expand)	Author
2001-08-05	Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction	herbelin
2001-08-05	Suppression des TmpHyp disgracieuses dans Decompose; utilisation de combinate...	herbelin
2001-08-05	Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...	herbelin
2001-08-01	Ajout code pour un Destruct similaire au NewInduction	herbelin
2001-07-13	Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne p...	herbelin
2001-07-10	Branchement sur bad_tactic_args	herbelin
2001-07-10	Branchement sur bad_tactic_args	herbelin
2001-07-10	Ajout du .ml pour la tactique Setoid_replace	clrenard
2001-07-10	Changement de place de la tactique Setoid_rewrite et renommage	clrenard
2001-07-04	ajout Show Intro(s)	letouzey
2001-06-29	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras
2001-06-29	traitement du let dans red_product (tactique Red)	barras
2001-06-27	commit d'un bug de Apply.	barras
2001-06-25	Refine sur les CoFix	filliatr
2001-06-25	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin
2001-06-25	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin
2001-06-15	Fix d'un bug de Tauto	delahaye
2001-06-13	Prise en compte env local (et defs locales) dans Change	herbelin
2001-06-01	Correction d'un bug du a un Intros trop violent	delahaye
2001-06-01	Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ...	herbelin
2001-05-31	Amelioration - subjective - de l'affichage des Hint	herbelin
2001-05-28	Pretty -> Prettyp	filliatr
2001-05-25	Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types	herbelin
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-03	Changement de la structure des points fixes	barras
2001-04-24	Ajout du cas True->A\|-B	delahaye
2001-04-19	Fonction lookup enlevee	delahaye
2001-04-15	Mise en page	herbelin
2001-04-12	Ajout de _ dans les patterns d'intro	mohring
2001-04-12	Mis un message d'erreur explicite pour l'echec de Elim en cas	mohring
2001-04-03	Make it possible to perform proofs by induction even on non-inductive types,	bertot
2001-03-28	amelioration de la structure des univers	barras
2001-03-22	Problèmes de NewInduction	herbelin
2001-03-15	entetes	filliatr
2001-03-09	bug de refine: uncaught exception Array.sub	barras
2001-03-08	changement comparaison etats	filliatr
2001-03-06	Modification de e_give_exact pour eviter d'echouer sur l'unification	mohring
2001-03-06	eta-expansion	mohring
2001-03-06	EAutod (debug)	filliatr
2001-03-05	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	backtrack unification types et deplacement make_clenv_binding	filliatr
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-28	modif	mohring
2001-02-27	EAuto mixte (largeur puis profondeur)	mohring
2001-02-26	changement message d'erreur Abstract	filliatr
2001-02-26	Eauto version en largeur	mohring
2001-02-26	Abstract: on échoue si le but contient des existentielles	filliatr
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-16	Prise en compte noms longs dans SuperAuto	herbelin