coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	distinguer interp_cs et interp_setcs	letouzey	2003-10-06
*	oups	letouzey	2003-09-28
*	2 pbs de plus réglés concernant Setoid Ring:	letouzey	2003-09-28
*	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin	2003-09-26
*	suite (et fin) reparation Setoid Ring	letouzey	2003-09-22
*	tentative de rafraichissement de Setoid Ring	letouzey	2003-09-22
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Reparation de ring pour les setoides	clrenard	2002-06-19
*	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
*	Suppression de l'application de f_equal2 pour "mult" (non inversible);	herbelin	2002-04-05
*	reparation semi setoid ring	clrenard	2002-03-14
*	compat ocaml 3.03	filliatr	2001-12-13
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	GROS COMMIT:	barras	2001-11-05
*	Parsing	herbelin	2001-08-10
*	Ajout d'un Ring pour setoides	clrenard	2001-07-10
*	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin	2001-07-02
*	patch Claudio	filliatr	2001-05-28
*	réparation Ring (simplifications)	filliatr	2001-05-14
*	entetes	filliatr	2001-03-15
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	nouvelle implantation de la reduction	barras	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
*	rétablissement patch Claudio	filliatr	2001-02-05
*	retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...	filliatr	2001-02-02
*	Comment fixed	sacerdot	2001-01-12
*	Now reduction to normal form is done only when the term is not	sacerdot	2001-01-11
*	Many unuseful rewritings are no more done by Ring.	sacerdot	2001-01-11
*	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
*	certains effets disparaissent a la sortie des sections, d'autres non (selon S...	filliatr	2000-11-24
*	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...	herbelin	2000-11-22
*	Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...	herbelin	2000-11-20
*	methode export	filliatr	2000-11-15
*	Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...	herbelin	2000-11-10
*	Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'	herbelin	2000-10-26
*	Manquait le cas Constr de dyn_polynom	herbelin	2000-10-25
*	Renommage AppL en App	herbelin	2000-10-01
*	Disparition du type oper mais nouveau type global_reference	herbelin	2000-10-01
*	Abstraction de constr	herbelin	2000-09-14
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
*	Suppression de Abst	herbelin	2000-09-10
*	Ring	filliatr	2000-06-21