coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.v	herbelin	2002-05-29
*	Ajout Peano_dec et Compare_dec	herbelin	2002-05-16
*	suppression de inf_decidable dans ZArith_dec (pour SeachPattern)	filliatr	2002-05-16
*	petite erreur de syntaxe	barras	2002-05-14
*	ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite	barras	2002-05-14
*	encore des lemmes sur Zdiv	filliatr	2002-05-14
*	nouveaux lemmes dans Zdiv (Claude Marche)	filliatr	2002-05-14
*	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr	2002-05-07
*	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr	2002-05-07
*	Cosmétique	herbelin	2002-05-06
*	Standardisation	herbelin	2002-05-06
*	lemmes sur Zdiv/Zmod	filliatr	2002-04-19
*	un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...	filliatr	2002-04-19
*	* empty log message *	werner	2002-04-17
*	Quelques bugs avec inject_nat	herbelin	2002-04-17
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Zdiv -> Export ZArith	filliatr	2002-04-08
*	syntaxe pour Zdiv et Zmod	filliatr	2002-04-08
*	simplification preuve	filliatr	2002-04-05
*	nouveau module Zdiv	filliatr	2002-04-05
*	Optimisation	desmettr	2002-04-02
*	Suppression PI_lb et PI_ub	desmettr	2002-04-02
*	Suppression Field	desmettr	2002-04-02
*	sans utiliser Field	desmettr	2002-03-29
*	Suppression des invocations a Field	desmettr	2002-03-29
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
*	* empty log message *	werner	2002-03-22
*	Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...	herbelin	2002-03-22
*	Intuition ne fait plus de Unfold des constantes (il faut les faire	courant	2002-03-21
*	Intuition now takes an (optional) tactic as parameter. This tactic is	courant	2002-03-20
*	Exportation de SplitRmult et SplitAbsolu	delahaye	2002-03-19
*	Field ne fait maintenant que les reductions necessaires	delahaye	2002-03-17
*	Ajout de lemmes	mohring	2002-03-13
*	* empty log message *	desmettr	2002-03-07
*	petits changements afin de profiter du nouveau Rewrite/in	barras	2002-03-05
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
*	Ajout andb_true_eq pour PolyList.list_beq	herbelin	2002-02-28
*	Doc + ajout fold_symmetric et nth_In	herbelin	2002-02-22
*	Doc	herbelin	2002-02-22
*	code mort dans tactinterp; plus de Debug On/Off dans Correctness	filliatr	2002-02-21
*	Uniformisation des theoremes dans Set et Type (def. de Acc_rect et	barras	2002-02-19
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	Syntaxe IF then else au lieu de either and_then or_else	barras	2002-02-14
*	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring	2002-01-31
*	modification de la definition des def inductives unitaires et autorisation d'...	mohring	2002-01-29
*	Bug affichage de O (de nat) dans une expression sur Z	herbelin	2002-01-25
*	Zdiv et Zmod dans Zcomplements	filliatr	2002-01-25
*	Bug commentaire (i i)	herbelin	2002-01-18
*	amadouage de coqweb	letouzey	2002-01-18
*	ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...	letouzey	2002-01-18