coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Restore documentation of library String which was removed in 2007 (r10049)	herbelin	2011-03-05
*	Remove obsolete TheoryList	glondu	2011-02-10
*	Fix formatting issue in refman	glondu	2011-01-12
*	Remove references to -ide option of coqmktop	glondu	2011-01-11
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	Precision in documentation of "decide equality"	glondu	2010-12-24
*	Remove the two-argument variant of "decide equality"	glondu	2010-12-23
*	More precise documentation for instantiate	glondu	2010-12-23
*	Example of a simple ML tactic (Hello world).	fkirchne	2010-12-09
*	Numbers and bitwise functions.	letouzey	2010-12-06
*	Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).	herbelin	2010-12-04
*	Documentation for tactic constr_eq	glondu	2010-12-02
*	Add tactic has_evar (#2433)	glondu	2010-12-02
*	Add tactic is_evar (Closes: #2433)	glondu	2010-12-02
*	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey	2010-11-19
*	Integer division: quot and rem (trunc convention) in addition to div and mod	letouzey	2010-11-10
*	Numbers: axiomatization, properties and implementations of gcd	letouzey	2010-11-05
*	Fix typo in "Hint Extern" doc	glondu	2010-11-03
*	Document DOT output of universe graph	glondu	2010-11-02
*	Numbers : log2. Abstraction, properties and implementations.	letouzey	2010-11-02
*	Move stuff about positive into a distinct PArith subdir	letouzey	2010-11-02
*	More precise description of boolean ring in doc (see bug #2401)	glondu	2010-10-11
*	TeX input method is now supported upstream	vgross	2010-10-07
*	Remove Explain* vernacs	glondu	2010-10-06
*	Remove VernacGo	glondu	2010-10-06
*	(Hopefully) clearer explanation of Ltac's context patterns	glondu	2010-10-05
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Minor fixes of 'make doc'	pboutill	2010-09-28
*	Added a section in the documentation of Vernacular commands about Set/Unset/T...	aspiwack	2010-09-23
*	Hopefully a fix for #2176 (redirection not understood with some shells)	herbelin	2010-09-19
*	Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for png...	emakarov	2010-09-06
*	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier	2010-07-28
*	Minor fixes:	msozeau	2010-07-27
*	Documentation of Set Automatic Coercions Import.	herbelin	2010-07-25
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	FSetPositive: sets of positive inspired by FMapPositive.	letouzey	2010-07-16
*	Updating reference manual credits: gb is now nsatz.	herbelin	2010-07-08
*	Update of documentation for the standard library (cf. #2332)	letouzey	2010-06-28
*	Applying François' patches about Canonical Projections (see #2302 and #2334).	herbelin	2010-06-26
*	modifs de nsatz suggerees par Hugo	pottier	2010-06-25
*	Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...	notin	2010-06-23
*	Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...	notin	2010-06-23
*	Documentation of clear dependent and revert dependent	letouzey	2010-06-18
*	Update of Extraction documentation	letouzey	2010-06-14
*	Extraction Implicit: documentation	letouzey	2010-06-14
*	Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.	herbelin	2010-06-11
*	Fixed a very old (from V6.3) typo in headers.sty	herbelin	2010-06-10
*	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin	2010-06-08
*	Backporting part of r12970 to trunk (deprecation of double induction).	herbelin	2010-06-07
*	doc Nstaz updated	pottier	2010-06-04