coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin	2001-06-25
*	liste des equiv exportee	clrenard	2001-06-25
*	Bug dépendances non pertinentes (dû à des K-rédex) dans le type des branc...	herbelin	2001-06-25
*	2 bugs: typevarlist pour inductifs + args pour flexibles	letouzey	2001-06-22
*	Ajout d'un Setoid_rewrite et meilleure resolution des petits sous-buts géné...	clrenard	2001-06-20
*	Normalisation du predicat synthetise pour les Case	clrenard	2001-06-20
*	oubli de Elimdep dans le Makefile	barras	2001-06-20
*	Un bug corrige.	clrenard	2001-06-19
*	Ajouts des theories du paradoxe de Berardi	delahaye	2001-06-19
*	Extension des parametres de Clear + Inst	delahaye	2001-06-19
*	Extension des parametres de Clear	delahaye	2001-06-19
*	Oubli Save + je sais plus	mayero	2001-06-19
*	Ajouts de lemmes (pour Float)	mayero	2001-06-18
*	Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)	barras	2001-06-18
*	Interpretation MetaId + Progress + Inst	delahaye	2001-06-18
*	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