coq - The formal proof system

Age	Commit message (Expand)	Author
2003-10-22	Ajout NArithRing	herbelin
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-10-06	distinguer interp_cs et interp_setcs	letouzey
2003-10-03	Cacher les .v8	herbelin
2003-09-28	oups	letouzey
2003-09-28	2 pbs de plus réglés concernant Setoid Ring:	letouzey
2003-09-26	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin
2003-09-22	commit accidentel d'une bidouille	letouzey
2003-09-22	suite (et fin) reparation Setoid Ring	letouzey
2003-09-22	tentative de rafraichissement de Setoid Ring	letouzey
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-05-21	Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...	herbelin
2003-05-21	Mise en conformite de la precedence du '-' unaire avec celle de Notations	herbelin
2003-05-21	Mise en conformite de la precedence du '-' unaire avec celle de Notations	herbelin
2003-05-21	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-05-13	Notations arithmetiques	herbelin
2003-04-09	Alignement du comportement des implicites d'inductif en sortie de section sur...	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2003-03-29	eq fusionne avec eqT et devient par défaut sur Type,	herbelin
2003-03-12	* empty log message *	barras
2002-12-02	Remplacement Grammar par Notation	herbelin
2002-12-02	Remplacement de Syntactic Definition par Notation	herbelin
2002-11-28	Nettoyage	herbelin
2002-11-26	Remplacement des Grammar et des [\| \|] par des notations	herbelin
2002-11-24	Nettoyage	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-06-20	ZArith_base, Zbool, Bool_nat	filliatr
2002-06-19	Reparation de ring pour les setoides	clrenard
2002-06-03	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin
2002-05-29	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-15	- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogus	barras
2002-04-17	Uniformisation (Qed/Save et Implicits Arguments)	herbelin
2002-04-05	Suppression de l'application de f_equal2 pour "mult" (non inversible);	herbelin
2002-03-14	reparation semi setoid ring	clrenard
2002-03-04	Nouveau Rewrite-in plus economique	barras
2001-12-13	compat ocaml 3.03	filliatr
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-21	Make sure that NatRing won't loop forever.	bertot
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-18	Modification de l'emplacement des fichiers pour les setoides.	clrenard
2001-09-14	MAJ vis à vis de la nouvelle non-localité des Remark/Fact	herbelin
2001-08-10	Parsing	herbelin
2001-08-07	Passage au nouveau Destruct	herbelin
2001-08-05	Expérimentation de NewDestruct et parfois NewInduction	herbelin