coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	code mort	herbelin	2001-06-16
*	Fix d'un bug de Tauto	delahaye	2001-06-15
*	plus besoin de separer les ?	barras	2001-06-13
*	Prise en compte env local (et defs locales) dans Change	herbelin	2001-06-13
*	Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes aut...	clrenard	2001-06-12
*	Ajout des entrees puor Setoid_replace.	clrenard	2001-06-12
*	Ajout de la tactique Setoid_replace.	clrenard	2001-06-12
*	Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Case	clrenard	2001-06-11
*	Fix de quelques bugs syntaxiques de Ltac	delahaye	2001-06-11
*	Ajout de deux anciens bugs	delahaye	2001-06-05
*	Correction bug outside	mayero	2001-06-04
*	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
*	Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant l...	herbelin	2001-05-31
*	Amelioration - subjective - de l'affichage des Hint	herbelin	2001-05-31
*	Retablissement de minicoq	coq	2001-05-29
*	Facilites pour le debogguage des univers.	coq	2001-05-29
*	Chgt de MAKE= ...	letouzey	2001-05-29
*	Correction d'un bug du pretty-print	clrenard	2001-05-29
*	option -byte	filliatr	2001-05-28
*	Pretty -> Prettyp	filliatr	2001-05-28
*	option -quality	filliatr	2001-05-28
*	patch Claudio	filliatr	2001-05-28
*	nettoyage	filliatr	2001-05-28
*	Oups: flingait les Dglob dans optimize	letouzey	2001-05-25
*	erreur DeBruijn causant un RecursionNotOnInductiveType quand le type est un Let	letouzey	2001-05-25
*	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
*	maj	letouzey	2001-05-22
*	suite du musée des horreurs	letouzey	2001-05-22
*	ordre des inductifs + axiome-type	letouzey	2001-05-22
*	Erreur dans un commentaire ...	clrenard	2001-05-18
*	Modification afin de permettre plusieurs modifs successives d'une commande	clrenard	2001-05-18
*	Correction d'un commentaire erroné.	clrenard	2001-05-16
*	Ajout d'une fonction de remplacement d'un sous-terme par un terme.	clrenard	2001-05-15
*	Modification pour passage p-automates	mohring	2001-05-15
*	Correction bug predicat du Cases (suite)	herbelin	2001-05-15
*	mise en place extraction haskell	filliatr	2001-05-14
*	réparation Ring (simplifications)	filliatr	2001-05-14
*	Bug propagation du predicat des Cases	herbelin	2001-05-12
*	Oubli d'hypotheses pour faire fonctionner les exemples	herbelin	2001-05-12
*	Oubli d'hypotheses pour faire fonctionner les exemples	herbelin	2001-05-12
*	application patch Claudio	filliatr	2001-05-11
*	bug cast	letouzey	2001-05-11
*	m.a.j. PROBLEMES/TODO	letouzey	2001-05-11
*	construct_reference regarde d'abord dans le contexte local, puis les globaux	filliatr	2001-05-11
*	exemples Magic	letouzey	2001-05-10
*	message 'is defined' seulement en mode verbose	filliatr	2001-05-10
*	retouche de extract_inductive_declaration	letouzey	2001-05-10
*	ajout d'un afficher de contexte et d'une fonction constbody_of_string	letouzey	2001-05-10