coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-12	MAJ	herbelin
2003-11-12	Idtac peut prendre un argument à afficher	narboux
2003-11-12	On sait jamais	herbelin
2003-11-12	conseille l'utilisation de la release officielle 2.2.0 de lablgtk	letouzey
2003-11-12	petits changements de syntaxe	barras
2003-11-12	deux doigts d'extraction dans le CHANGES pour la V8	letouzey
2003-11-12	les modifs depuis la 7.4	letouzey
2003-11-12	TODO	letouzey
2003-11-12	Extraction Module M devient simplement Extraction M	letouzey
2003-11-11	maj	filliatr
2003-11-10	MAJ OTHERFLAGS	herbelin
2003-11-10	Re-suppression de is_verbose dans Print, pour coqide	herbelin
2003-11-10	Suppression SearchNamed finalement redondant avec SearchAbout	herbelin
2003-11-10	le pb du <<.v vu comme module>> engendre maintenant une erreur	letouzey
2003-11-10	message informant de l'ecriture d'un fichier extrait	letouzey
2003-11-10	révision du traitement des axiomes non réalisés	letouzey
2003-11-10	maj	filliatr
2003-11-10	essai d'extraction sous un module	letouzey
2003-11-09	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-08	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-07	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-06	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-05	Notations	herbelin
2003-11-05	Interpretation des entiers dans N (ex-entier), maj du module des positive	herbelin