coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Renommage des variables dans les schémas d'induction	herbelin	2001-02-14
*	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin	2001-02-14
*	- coqc : option -image	filliatr	2001-02-01
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Mise a jour Rbase	mohring	2001-01-11
*	Changement dans les noms longs (2eme)	herbelin	2000-11-29
*	Changement dans les noms longs	herbelin	2000-11-29
*	Nouveau long long avec Coq en tête	herbelin	2000-11-29
*	Prise en compte du repertoire dans le section path; utilisation de dirpath po...	herbelin	2000-11-28