coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Ordre standard pour l'associativite	herbelin	2003-11-14
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	Noms/énoncés plus canoniques	herbelin	2003-11-12
*	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...	herbelin	2003-11-05
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30
*	Ajout notations pour les expressions dans un anneau	herbelin	2003-10-28
*	Simplification preuve	herbelin	2003-10-28
*	Ajout NArithRing	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	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
*	Cacher les .v8	herbelin	2003-10-03
*	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
*	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-22
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-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-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Notations arithmetiques	herbelin	2003-05-13
*	Alignement du comportement des implicites d'inductif en sortie de section sur...	herbelin	2003-04-09
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea	2003-03-31
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	* empty log message *	barras	2003-03-12
*	Remplacement Grammar par Notation	herbelin	2002-12-02
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-12-02
*	Nettoyage	herbelin	2002-11-28
*	Remplacement des Grammar et des [\| \|] par des notations	herbelin	2002-11-26
*	Nettoyage	herbelin	2002-11-24
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	ZArith_base, Zbool, Bool_nat	filliatr	2002-06-20
*	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
*	Fichiers contrib//.ml4 remplacent les contrib//.v	herbelin	2002-05-29
*	- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogus	barras	2002-05-15
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Suppression de l'application de f_equal2 pour "mult" (non inversible);	herbelin	2002-04-05
*	reparation semi setoid ring	clrenard	2002-03-14
*	Nouveau Rewrite-in plus economique	barras	2002-03-04
*	compat ocaml 3.03	filliatr	2001-12-13