coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	added a lemma to prove inj_pair2 when eq_dec is available.	vsiles	2007-09-26
*	Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc,	notin	2007-06-21
*	Passage de Set à Type dans Relations et Wellfounded	herbelin	2007-02-06
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
*	Mise en forme des theories	notin	2006-10-17
*	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin	2006-03-05
*	Nouvelle en-tête	herbelin	2004-07-16
*	simplified proof (eq and eqT are now the same)	barras	2004-06-25
*	eq2eqT et eqT2eq devenus obsolètes	herbelin	2004-06-02
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)	barras	2001-06-18
*	Mise de (*i autour CVS info	mohring	2001-04-19
*	documentation automatique de la bibliothèque standard	filliatr	2001-04-11
*	entetes	filliatr	2001-03-15
*	Renommage des variables dans les schémas d'induction	herbelin	2001-02-14
*	caractere opaque des constantes repris en compte	filliatr	2000-12-04
*	Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...	herbelin	2000-03-21
*	Syntactic Definition n'etaient pas correctemenet importees	filliatr	2000-03-16
*	* empty log message *	barras	2000-03-10
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21