coq - The formal proof system

Age	Commit message (Expand)	Author
2006-01-21	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-19	Correction associativité de IF et exists (visible à l'affichage uniquement ...	herbelin
2005-12-22	Contrepartie de la suppression des boites automatiques dans format	herbelin
2005-11-30	changement parametres inductifs dans les theories	mohring
2005-08-26	* empty log message *	letouzey
2005-05-19	Documentation	herbelin
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin
2005-03-31	Added option_map	herbelin
2005-02-23	quelques tactics ltac	letouzey
2005-02-04	Essai d'utilisation de 'where' pour les notations	herbelin
2005-02-03	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
2004-12-06	Inutile de réserver les notations à base de '{ }'	herbelin
2004-11-12	Changement dans les boxed values .	gregoire
2004-08-01	Commentaires coqdoc	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-04-06	sumbool et sumor affich avec 'if' si possible	herbelin
2004-03-29	Commentaires	herbelin
2004-03-17	Definition de la notation de la paire par un motif recursif	herbelin
2004-02-28	MAJ Commentaires	herbelin
2004-02-12	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin
2004-01-09	Commentaires en v8	herbelin
2003-12-23	Finalement, espacement autour du ':' pour a la fois exists, forall et fun	herbelin
2003-12-21	Affichage sur le modèle du forall pour le exists	herbelin
2003-12-16	Duplication temporaire des règles de syntaxe des paires	herbelin
2003-12-15	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras
2003-12-05	power associe a droite	marche
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-21	Tri et typo	herbelin
2003-11-14	Automatisation de la traduction de iff_trans; renommage IF	herbelin
2003-11-14	Backtrack sur Peano	herbelin
2003-11-13	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras
2003-11-12	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-01	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin
2003-10-30	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin
2003-10-28	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	Ajout %core; MAJ niveau connecteurs logique	herbelin
2003-10-23	Commentaires	herbelin
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-21	Maintenant avant Datatypes	herbelin
2003-10-21	ajouts	herbelin
2003-10-17	Des implicites plus 'naturels' pour eq_ind, identity_ind and co	herbelin
2003-10-16	nouvelle syntaxe de ltac	barras
2003-10-14	Changement 'as notation' en 'where notation'	herbelin