coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin	2009-01-13
*	Fixed two problems:	herbelin	2009-01-03
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	About "apply in":	herbelin	2008-12-09
*	- Fixed many "Theorem with" bugs.	herbelin	2008-10-27
*	Fix doc of apply in (see coq-club message 26 September 2008)	herbelin	2008-10-24
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	Add user syntax for creating hint databases [Create HintDb foo	msozeau	2008-09-14
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Lissage de la gestion des chemins de chargement de fichiers :	herbelin	2008-06-29
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	Fix a typo	glondu	2008-06-09
*	Documentation de "instantiate".	glondu	2008-06-09
*	- Documentation de admit et Print Assumptions.	herbelin	2008-06-09
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in	letouzey	2008-06-01
*	remove additional occurrences of +/- forgotten in commit 11030	letouzey	2008-06-01
*	Bactrack sur +, - dans rewrite qui, redondants avec ->, <-, n'en sont qu'à	herbelin	2008-06-01
*	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau	2008-05-12
*	Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour	herbelin	2008-04-26
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	* added a subsection to explain the automatic declaration of schemes:	vsiles	2008-04-15
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
*	typo	vsiles	2008-04-15
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Indexation de pose proof, et par la même occasion du nouveau specialize	herbelin	2008-03-10
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	repair for commit 10612 (due to grammar order, some syntaxes weren't working)	letouzey	2008-03-06
*	Rework on rich forms of rewrite	letouzey	2008-03-01
*	Add new files theories/Program/Basics.v and theories/Classes/Relations.v	msozeau	2008-02-03
*	Debug implementation of dependent induction/dependent destruction and documen...	msozeau	2008-01-31
*	Standardisation du format des références croisées vers Figure, Section, Ch...	herbelin	2008-01-05
*	Added the doc for the new Scheme Equality command	vsiles	2007-10-16
*	Indication de quel type de constantes est dépliable dans "simpl" (cf	herbelin	2007-09-19
*	More natural notation for intro pattern: @a -> ?a	glondu	2007-07-09
*	Adding a syntax for "n-ary" rewrite:	letouzey	2007-07-06
*	extension of the rename tactic: the following is now allowed:	letouzey	2007-07-06
*	New intro pattern "@A", which generates a fresh name based on A.	glondu	2007-07-06
*	Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))	letouzey	2007-07-06
*	documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/...	letouzey	2007-07-05
*	Removed an extra \tacindex occurrence for the tactic discriminate.	emakarov	2007-06-08
*	Ajout doc clear sans argument	herbelin	2007-06-07
*	Made some places in the reference manual clearer. Corrected	emakarov	2007-05-11
*	Fixed some typos.	glondu	2007-04-18
*	Changed many refman/*.tex files. Put \label and \index commands that immediat...	emakarov	2007-04-17
*	Cleaned doc/common/title.tex file. Increased the space under headers	emakarov	2007-04-12
*	Mise en place d'un rafinement de compute.	jforest	2007-04-05
*	Correction bug #1439 (comportement de replace by)	notin	2007-03-13