coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	MAJ	herbelin	2006-03-05
*	Ajout 'exists! x:A, P	herbelin	2006-02-23
*	Nettoyage Zmin.v, création Zmax.v et Zminmax.v	herbelin	2006-02-12
*	Ajout bibliothèque String de Laurent Théry	herbelin	2006-02-08
*	Idem numbering of 'Unfold', 'simpl', ...	herbelin	2006-02-07
*	Mise en conformité de l'ordre des occurrences de pattern avec l'affichage	herbelin	2006-02-07
*	MAJ	herbelin	2006-02-07
*	coq_makefile	herbelin	2006-02-06
*	MAJ (synonymes de Lemma; auto using)	herbelin	2006-01-29
*	Export eassumption	herbelin	2006-01-19
*	Extended Unicode support	herbelin	2006-01-19
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom	herbelin	2006-01-16
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
*	Ajout paramétricité du nom de la base de hint dans auto et trivial	herbelin	2006-01-11
*	MAJ	herbelin	2006-01-07
*	Suppression des parseurs et printeurs v7; suppression du traducteur; changeme...	herbelin	2005-12-26
*	* empty log message *	herbelin	2005-12-23
*	MAJ	herbelin	2005-12-21
*	Declare Implicit Tactic	herbelin	2005-09-09
*	add a left and right tactic for classical logic	narboux	2005-07-15
*	fold	herbelin	2005-07-15
*	Added entry constr_may_eval for tactic extensions (new syntax)	herbelin	2005-06-22
*	New environment variable COQREMOTEBROWSER to set the command used by Coq	sacerdot	2005-05-26
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
*	Implemented autorewrite with ... in hyp [using ...].	sacerdot	2005-05-18
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	possibilité d'écrire [foo\| ] au lieu de [foo\|idtac]	letouzey	2005-05-09
*	Fixed hypotheses of Z_lt_induction (see #957)	herbelin	2005-04-26
*	Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...	herbelin	2005-03-29
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin	2005-03-07
*	Renaming Print Canonical Structure into Print Canonical Projections	herbelin	2005-02-18
*	Ajout Print Canonical Structures	herbelin	2005-02-12
*	Nettoyage et documentation de Library	herbelin	2005-02-06
*	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot	2005-01-13
*	- Module/Declare Module syntax made more uniform:	sacerdot	2005-01-06
*	HUGE COMMIT	sacerdot	2005-01-03
*	Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)	herbelin	2004-12-27
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
*	Ajout 'Locate Module'	herbelin	2004-11-17
*	MAJ	herbelin	2004-11-09
*	Prise en compte des notations récursives dans l'option 'format'	herbelin	2004-11-08
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	Incorrection exportation XML	herbelin	2004-04-17
*	Finalement pas de liste des contributions (cela n'avait été fait que pour l...	herbelin	2004-04-17
*	Nouvelles majs	herbelin	2004-04-16
*	MAJ	herbelin	2004-04-14
*	MAJ	herbelin	2004-03-28
*	MAJ	herbelin	2004-03-17
*	preparation pour release (suite)	barras	2004-03-15