coq - The formal proof system

Age	Commit message (Expand)	Author
2007-10-05	Added the automatic generation of the boolean equality if possible and the	vsiles
2007-10-03	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2007-08-08	Fix dependency bugs due to Program modules renamings.	msozeau
2007-08-07	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau
2007-06-22	Ajout exist & cie à la table des hints par symétrie avec ex_intro &	herbelin
2007-06-08	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov
2007-06-05	Gestion espaces dans notation _ = _ :> _	herbelin
2007-04-28	Déplacement des opérations sur bool dans l'état initial	herbelin
2007-04-02	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov
2007-04-01	Removed the definition of extensions of apply to equivalences	emakarov
2007-03-30	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov
2007-03-26	stupid me: ?f two times in a pattern	letouzey
2007-01-02	Add f_equal case for 6 arguments.	msozeau
2006-10-24	Ajout de la tactique 'remember'	herbelin
2006-10-17	Mise en forme des theories	notin
2006-10-05	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey
2006-09-22	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin
2006-09-21	incomplete and temporary fix for PR#1222: revert accepts up to 10 args	letouzey
2006-08-28	Passage à une définition de inhabited plus dans les 'standard mathématique...	herbelin
2006-06-25	repetition d'hypotheses dans well_founded_induction_type_2	letouzey
2006-06-09	Modification déf de exists! pour éviter une éta-expansion et pouvoir être...	herbelin
2006-06-04	Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...	herbelin
2006-06-04	Ajout exists! et restructuration/extension des fichiers sur la	herbelin
2006-05-29	Ajout d'alias pour prodT_rect et cie qui avaient Ã©tÃ© oublkÃiÃ©s	herbelin
2006-05-28	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-03-17	Modification des propriétés (svn:executable)	notin
2006-03-04	Titres moins envahissants pour coqdoc	herbelin
2006-02-27	quelques raccourcis commodes + un f_equal plus efficace	letouzey
2006-02-23	Ajout 'exists! x:A, P (suite)	herbelin
2006-02-23	Ajout 'exists! x:A, P	herbelin
2006-02-10	code mort	herbelin
2006-02-06	Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...	herbelin
2006-01-22	Application de la suggestion de Nicolas Magaud (#1060)	herbelin
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