coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	La correction precedente a mis en evidence un defaut de l'utilisation de intr...	herbelin	2003-12-24
*	Renommages des hypotheses transformees car en raison des possibles dependance...	herbelin	2003-12-23
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Restructuration ZArith	herbelin	2003-11-12
*	Déport des lemmes de Omega de ZArith vers OmegaLemmas	herbelin	2003-11-05
*	Extension de zarith	herbelin	2003-11-04
*	Construction des chemins de constantes plus robuste	herbelin	2003-10-21
*	Cacher les .v8	herbelin	2003-10-03
*	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin	2003-09-26
*	Globalisation de ce qui n'etait pas encore globalise	herbelin	2003-06-10
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	commentaires	herbelin	2003-04-17
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
*	minus a changé d'emplacement -> omega pas content	letouzey	2003-03-31
*	* empty log message *	barras	2003-03-12
*	Auto with zarith essaye Abstract Omega sur un but False	filliatr	2003-01-30
*	Problèmes et améliorations divers affichage	herbelin	2002-12-09
*	Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...	herbelin	2002-10-23
*	Meilleure lisibilité grâce à tclTHENLIST	herbelin	2002-10-19
*	Réparation bug #180	herbelin	2002-10-19
*	Omega can now elim hyps of type False. Therefore, it knows how to deal	courant	2002-10-02
*	Un peu (plus) d'ordre dans Nametab...	coq	2002-09-24
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	ZArith_base, Zbool, Bool_nat	filliatr	2002-06-20
*	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin	2002-06-03
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
*	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin	2002-04-11
*	Uniformisation convert_hyp	herbelin	2002-02-28
*	patch Omega (bug 129)	filliatr	2002-01-25
*	Correction de Pierre Crégut pour le bug MERGE_EQ	herbelin	2002-01-21
*	Bug MERGE_EQ	herbelin	2002-01-18
*	ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...	letouzey	2002-01-18
*	compat ocaml 3.03	filliatr	2001-12-13
*	GROS COMMIT:	barras	2001-11-05
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Transparent	barras	2001-09-20
*	Nettoyage reduce_to_ind et one_step_reduce	herbelin	2001-09-09
*	Parsing	herbelin	2001-08-10
*	Expérimentation de NewDestruct et parfois NewInduction	herbelin	2001-08-05
*	correction bug Omega	filliatr	2001-07-05
*	remplace Zarith par ZArith	mohring	2001-04-19
*	portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega	filliatr	2001-04-10
*	Ajout lemmes arithmetiques	mohring	2001-04-08
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01