coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Fix dependency bugs due to Program modules renamings.	msozeau	2007-08-08
*	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau	2007-08-07
*	Ajout exist & cie à la table des hints par symétrie avec ex_intro &	herbelin	2007-06-22
*	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov	2007-06-08
*	Gestion espaces dans notation _ = _ :> _	herbelin	2007-06-05
*	Déplacement des opérations sur bool dans l'état initial	herbelin	2007-04-28
*	Added back the tactics [apply -> ident], etc. to Tactics.v after	emakarov	2007-04-02
*	Removed the definition of extensions of apply to equivalences	emakarov	2007-04-01
*	Added new tactics for applying equivalences (iff) to Tactics.v:	emakarov	2007-03-30
*	stupid me: ?f two times in a pattern	letouzey	2007-03-26
*	Add f_equal case for 6 arguments.	msozeau	2007-01-02
*	Ajout de la tactique 'remember'	herbelin	2006-10-24
*	Mise en forme des theories	notin	2006-10-17
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
*	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin	2006-09-22
*	incomplete and temporary fix for PR#1222: revert accepts up to 10 args	letouzey	2006-09-21
*	Passage à une définition de inhabited plus dans les 'standard mathématique...	herbelin	2006-08-28
*	repetition d'hypotheses dans well_founded_induction_type_2	letouzey	2006-06-25
*	Modification déf de exists! pour éviter une éta-expansion et pouvoir être...	herbelin	2006-06-09
*	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-06-04
*	Ajout d'alias pour prodT_rect et cie qui avaient Ã©tÃ© oublkÃiÃ©s	herbelin	2006-05-29
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	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