coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Quelqes renommages lies a Zorder	herbelin	2003-11-09
*	Ajout quelques lemmes; noms des variables liees	herbelin	2003-11-09
*	make moins verbeux, suite (et fin?)	letouzey	2003-11-09
*	factorisation de (recursive) library	letouzey	2003-11-09
*	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin	2003-11-09
*	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin	2003-11-09
*	Traduction semantique des InHyp de clause en InHypValue si local def; simplif...	herbelin	2003-11-09
*	Mise en place traduction des tactiques apres evaluation pour permettre des ch...	herbelin	2003-11-09
*	'as' avant 'using' dans 'destruct'	herbelin	2003-11-09
*	Test Generalize	herbelin	2003-11-09
*	Ajout pf_apply	herbelin	2003-11-09
*	Ajout reduce_to_quantified_ref	herbelin	2003-11-09
*	'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ...	herbelin	2003-11-09
*	Code obsolete	herbelin	2003-11-08
*	Fusion de tuple_constr/tuple_pattern dans operconstr/pattern	herbelin	2003-11-08
*	MAJ	herbelin	2003-11-08
*	Nettoyage	herbelin	2003-11-08
*	Ajout option -impredicative-set	herbelin	2003-11-08
*	Suppression StronglyClassical, StronglyConstructive devient plus concretement...	herbelin	2003-11-08
*	maj	filliatr	2003-11-08
*	Oubli BinNat	herbelin	2003-11-07
*	Oubli d'un Set Implicit Arguments	herbelin	2003-11-07
*	Biblio standard sans mention de la possibilite d'etre impredicatif; Hurkens_s...	herbelin	2003-11-07
*	Biblio standard sans mention de la possibilite d'etre impredicatif	herbelin	2003-11-07
*	Biblio standard sans impredicativite	herbelin	2003-11-07
*	maj	filliatr	2003-11-07
*	Added Instantiate ... in	corbinea	2003-11-06
*	Des oublis	herbelin	2003-11-06
*	Report des definitions sorties de fast_integer pour compatibilite	herbelin	2003-11-06
*	maj	filliatr	2003-11-06
*	Notations	herbelin	2003-11-05
*	Interpretation des entiers dans N (ex-entier), maj du module des positive	herbelin	2003-11-05
*	Oubli	herbelin	2003-11-05
*	MAJ	herbelin	2003-11-05
*	2 espaces en trop	herbelin	2003-11-05
*	MAJ	herbelin	2003-11-05
*	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...	herbelin	2003-11-05
*	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...	herbelin	2003-11-05
*	Preuve de l'incoherence de {A}+{~A} avec Set impredicatif	herbelin	2003-11-05
*	Renommage canonique d'un lemme redondant	herbelin	2003-11-05
*	Redondances	herbelin	2003-11-05
*	Modules obsoletes de ZArith en v8	herbelin	2003-11-05
*	Nouvelle vague de renommage	herbelin	2003-11-05
*	Déport des lemmes de Omega de ZArith vers OmegaLemmas	herbelin	2003-11-05
*	Ajout NArith et restructuration ZArith	herbelin	2003-11-05
*	Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...	herbelin	2003-11-05
*	MAJ	herbelin	2003-11-05
*	Renommage canonique d'un lemme redondant	herbelin	2003-11-05
*	Branchement de Show Script sur l'afficheur structure	herbelin	2003-11-05
*	Amelioration de l'afficheur de script structure	herbelin	2003-11-05