coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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-05
*	Ajout code pour un Destruct similaire au NewInduction	herbelin	2001-08-01
*	Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne p...	herbelin	2001-07-13
*	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-10
*	ajout Show Intro(s)	letouzey	2001-07-04
*	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-29
*	commit d'un bug de Apply.	barras	2001-06-27
*	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-25
*	Fix d'un bug de Tauto	delahaye	2001-06-15
*	Prise en compte env local (et defs locales) dans Change	herbelin	2001-06-13
*	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-06-01
*	Amelioration - subjective - de l'affichage des Hint	herbelin	2001-05-31
*	Pretty -> Prettyp	filliatr	2001-05-28
*	Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types	herbelin	2001-05-25
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Changement de la structure des points fixes	barras	2001-05-03
*	Ajout du cas True->A\|-B	delahaye	2001-04-24
*	Fonction lookup enlevee	delahaye	2001-04-19
*	Mise en page	herbelin	2001-04-15
*	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-12
*	Make it possible to perform proofs by induction even on non-inductive types,	bertot	2001-04-03
*	amelioration de la structure des univers	barras	2001-03-28
*	Problèmes de NewInduction	herbelin	2001-03-22
*	entetes	filliatr	2001-03-15
*	bug de refine: uncaught exception Array.sub	barras	2001-03-09
*	changement comparaison etats	filliatr	2001-03-08
*	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-06
*	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr	2001-03-05
*	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-03-01
*	modif	mohring	2001-02-28
*	EAuto mixte (largeur puis profondeur)	mohring	2001-02-27
*	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-26
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Prise en compte noms longs dans SuperAuto	herbelin	2001-02-16