coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	Titres moins envahissants pour coqdoc	herbelin	2006-03-04
*	quelques raccourcis commodes + un f_equal plus efficace	letouzey	2006-02-27
*	Ajout 'exists! x:A, P (suite)	herbelin	2006-02-23
*	Ajout 'exists! x:A, P	herbelin	2006-02-23
*	code mort	herbelin	2006-02-10
*	Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...	herbelin	2006-02-06
*	Application de la suggestion de Nicolas Magaud (#1060)	herbelin	2006-01-22
*	Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es...	herbelin	2006-01-21
*	Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc	herbelin	2006-01-21
*	Correction associativité de IF et exists (visible à l'affichage uniquement ...	herbelin	2006-01-19
*	Contrepartie de la suppression des boites automatiques dans format	herbelin	2005-12-22
*	changement parametres inductifs dans les theories	mohring	2005-11-30
*	* empty log message *	letouzey	2005-08-26
*	Documentation	herbelin	2005-05-19
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Added option_map	herbelin	2005-03-31
*	quelques tactics ltac	letouzey	2005-02-23
*	Essai d'utilisation de 'where' pour les notations	herbelin	2005-02-04
*	Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs	herbelin	2005-02-03
*	Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs	herbelin	2005-02-03
*	Inutile de réserver les notations à base de '{ }'	herbelin	2004-12-06
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Commentaires coqdoc	herbelin	2004-08-01
*	Nouvelle en-tête	herbelin	2004-07-16
*	sumbool et sumor affich avec 'if' si possible	herbelin	2004-04-06
*	Commentaires	herbelin	2004-03-29
*	Definition de la notation de la paire par un motif recursif	herbelin	2004-03-17
*	MAJ Commentaires	herbelin	2004-02-28
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
*	Commentaires en v8	herbelin	2004-01-09
*	Finalement, espacement autour du ':' pour a la fois exists, forall et fun	herbelin	2003-12-23
*	Affichage sur le modèle du forall pour le exists	herbelin	2003-12-21
*	Duplication temporaire des règles de syntaxe des paires	herbelin	2003-12-16
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	power associe a droite	marche	2003-12-05
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Tri et typo	herbelin	2003-11-21
*	Automatisation de la traduction de iff_trans; renommage IF	herbelin	2003-11-14
*	Backtrack sur Peano	herbelin	2003-11-14
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	Ajout lemme projections	herbelin	2003-11-12
*	%type au lieu de %T	herbelin	2003-11-12
*	Lemmes dans un sens plus naturel	herbelin	2003-11-12
*	petits changements de syntaxe	barras	2003-11-12
*	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
*	Ordre (symbolique) des Require	herbelin	2003-10-28
*	Passage de la notations de paire dans core_scope	herbelin	2003-10-28
*	Passage des notations de type dans type_scope	herbelin	2003-10-28