coq - The formal proof system

Age	Commit message (Expand)	Author
2003-10-10	Plus d'Eval Compute	herbelin
2003-10-03	Cacher les .v8	herbelin
2003-10-01	Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...	herbelin
2003-09-30	'_ = _ = _' maintenant predefini, meme en V7	herbelin
2003-09-26	'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...	herbelin
2003-09-26	Structuration de fast_integer en operations sur positive, proprietes des oper...	herbelin
2003-09-25	add_x_x de fast_integer vers auxiliary	herbelin
2003-09-25	Retour provisoire a une section	herbelin
2003-09-24	Suppression section, ce qui evite de repliquer les declarations d'Infix	herbelin
2003-09-24	Destruct -> NewDestruct	herbelin
2003-09-22	Deplacement de lemmes de IntMap vers ZArith	herbelin
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-21	Conflit de nom Pplus dans positive et dans polynomial (de ring)	herbelin
2003-09-21	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...	herbelin
2003-09-19	Section et report Infix hors section	herbelin
2003-09-19	Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...	herbelin
2003-09-12	Bind et Delimit pour positive et Z (hors section)	herbelin
2003-09-05	principes de récurrences plus efficaces pour l'extraction	letouzey
2003-09-05	Zdiv plus efficace: r+r -> 2*r	letouzey
2003-09-05	Zabs_Zsgn	letouzey
2003-08-10	Un peu d'aide pour le traducteur	herbelin
2003-07-18	Coq.Init.Logic.eq au lieu de eq	filliatr
2003-07-08	recursion bien fondee sur des pairs	filliatr
2003-06-18	Arguments superflus pour Zlength_nil	herbelin
2003-06-14	Deplacement de le_minus de fast_integer vers Minus	herbelin
2003-06-13	FSets, mais pas compile' par make world	filliatr
2003-06-13	suite changements ZArith en vu de librairie FSet	letouzey
2003-06-13	quelques adaptations de Zarith en vu de la nouvelle librarie FSet	letouzey
2003-06-13	Deplacement d'un lemme sur nat de ZArith vers Arith	herbelin
2003-06-10	Import nat_scope	herbelin
2003-05-29	niveau 49 devient next	herbelin
2003-05-21	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin
2003-05-07	coqide: toolbar/autosave	monate
2003-04-09	Ajout Open Scope	herbelin
2003-04-09	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin
2003-04-09	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin
2003-03-28	Pas d'associativité gauche au niveau 3 en vieille syntaxe !	herbelin
2003-03-28	notations <>, Assumption avec existentiel, replace term	mohring
2003-03-21	* empty log message *	barras
2003-03-12	* empty log message *	barras
2003-02-13	Modifications dans une tactique toplevel	delahaye
2003-01-22	Bug precedence	herbelin
2003-01-21	Adaptation à la nouvelle sémantique plus uniforme de "Match term"	herbelin
2003-01-06	bit vectors	filliatr
2002-12-28	Re-installation nombres dans les motifs sur Z	herbelin
2002-12-15	Ajout syntaxe '>'	herbelin
2002-12-10	Compatibilite times1 (suite)	herbelin
2002-12-09	Nouvelle preuve de times_convert pour nouvelle définition de times	herbelin
2002-12-07	Compatibilité times1	herbelin
2002-12-06	Un axiome en attendant la mise a jour de la preuve de times_convert	herbelin