coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nouvelle en-tête	herbelin	2004-07-16
*	Retour sur amendement de l'interprétation mult sur nat (bug 743) car incompa...	herbelin	2004-05-28
*	Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de...	herbelin	2004-05-07
*	Reparation ROmega V8/Omega ZERO/POS/NEG	mohring	2004-03-04
*	Protection d'un 'clear' qui peut etre dependant	herbelin	2004-03-01
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	Nettoyage reduce_to_ind et one_step_reduce	herbelin	2001-09-09
*	Parsing	herbelin	2001-08-10
*	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
*	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin	2001-02-14
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	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
*	Appel des constantes globaux par des noms absolus	herbelin	2000-11-26
*	id_of_global devient sp_of_global	herbelin	2000-11-23