coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nouvelle en-tête	herbelin	2004-07-16
*	backtrack implicit dans Bvector	marche	2004-02-10
*	patch Bvector: args implicites	marche	2004-02-09
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
*	Duplication temporaire des règles de syntaxe des paires	herbelin	2003-12-16
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin	2003-12-04
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	ground->firstorder, cc-> congruence, CC final commit	corbinea	2003-11-29
*	Report de lemmes de Znumtheory dans Zabs ou BinInt	herbelin	2003-11-29
*	Renoncement de la compatibilite des noms qualifies au profit de la compatibil...	herbelin	2003-11-24
*	Compatibilite	herbelin	2003-11-22
*	Simplification; ajout Zcompare_antisym	herbelin	2003-11-21
*	ajout Pnat (suite)	herbelin	2003-11-21
*	ajout de Znumtheory.v dans ZArith	letouzey	2003-11-19
*	Un nouveau lemme redondant ...	herbelin	2003-11-18
*	Deplacement ZERO_le_inj dans Zorder	herbelin	2003-11-18
*	Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_base	herbelin	2003-11-14
*	cosmetique	herbelin	2003-11-14
*	Quelques oublis pour que les notations marchent bien	herbelin	2003-11-14
*	Bug implicit arguments	herbelin	2003-11-14
*	Oubli report Nul/Pos	herbelin	2003-11-13
*	Require	herbelin	2003-11-13
*	qq petit ajouts à Zdiv	letouzey	2003-11-13
*	Restructuration ZArith	herbelin	2003-11-12
*	Ajout lemmes; independance vis a vis noms variables liees; restructuration	herbelin	2003-11-12
*	Ajout partie sur bool anciennement dans Zmisc	herbelin	2003-11-12
*	Ajout lemmes; independance vis a vis noms variables liees	herbelin	2003-11-12
*	Ajout quelques lemmes; noms des variables liees	herbelin	2003-11-09
*	Oubli BinNat	herbelin	2003-11-07
*	Oubli d'un Set Implicit Arguments	herbelin	2003-11-07
*	Des oublis	herbelin	2003-11-06
*	Report des definitions sorties de fast_integer pour compatibilite	herbelin	2003-11-06
*	Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...	herbelin	2003-11-05
*	Exporting ^; utilisation arg scope implicite	herbelin	2003-11-03
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Retour en arriere sur d'autres renommages de variables	herbelin	2003-10-28
*	Retour a un nommage non standard des variables pour compatibilite; report 're...	herbelin	2003-10-27
*	Documentation/Structuration	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Redondance de dec_eq_nat	herbelin	2003-10-21
*	Type relation dans Datatypes	herbelin	2003-10-21
*	Suppression des surcharge de regles de grammaire en v7	herbelin	2003-10-16
*	Notations pour l'exponentiation	herbelin	2003-10-13
*	Plus d'Eval Compute	herbelin	2003-10-10
*	Cacher les .v8	herbelin	2003-10-03
*	Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...	herbelin	2003-10-01
*	'_ = _ = _' maintenant predefini, meme en V7	herbelin	2003-09-30
*	'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-26