coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	CHANGES: update of syntax for annotations of functor application	letouzey	2011-03-04
*	Extraction: improved indentation of extracted code (fix #2497)	letouzey	2011-03-04
*	Update changelogs	glondu	2011-02-11
*	Fixpoints are traverse during implicits arguments search to toplevel	pboutill	2011-02-10
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Update CHANGES	pboutill	2011-01-07
*	First release of Vector library.	pboutill	2010-12-10
*	ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2	letouzey	2010-12-09
*	Numbers and bitwise functions.	letouzey	2010-12-06
*	Document new tactics in CHANGES	glondu	2010-12-02
*	CHANGES: mention some changes in trunk since the 8.3 fork	letouzey	2010-11-19
*	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey	2010-11-19
*	CHANGES: small re-sync with the one of branch v8.3	letouzey	2010-11-19
*	Document DOT output of universe graph	glondu	2010-11-02
*	update CHANGES w.r.t. extraction	letouzey	2010-10-08
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Update CHANGES: Local/Global Set/Unset.	aspiwack	2010-09-23
*	Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +	herbelin	2010-09-02
*	Documentation of Set Automatic Coercions Import.	herbelin	2010-07-25
*	Made coercions active only when modules are imported.	herbelin	2010-07-22
*	Extraction Library Foo creates Foo.ml, not foo.ml	letouzey	2010-07-07
*	CHANGES: mention last-minute improvements of extraction	letouzey	2010-07-07
*	Remove dependency to Unix from module Profile	glondu	2010-07-02
*	Made "replace" accepts open terms on its left-hand-side.	herbelin	2010-06-28
*	Applying François' patches about Canonical Projections (see #2302 and #2334).	herbelin	2010-06-26
*	Commit 13179 continued (updated CHANGES about support for Heq's library).	herbelin	2010-06-22
*	Documentation of clear dependent and revert dependent	letouzey	2010-06-18
*	CHANGE: a word about new commands Compute and Fail	letouzey	2010-06-15
*	CHANGES: list of modifications for the extraction	letouzey	2010-06-15
*	Alert on the possible incompatibilties with set_add (see bug 2111) which	herbelin	2010-06-14
*	Keep description of Automatic Introduction at only one place of CHANGES.	herbelin	2010-06-09
*	Automatic introduction of names given before ":" in Lemma's and	herbelin	2010-06-09
*	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin	2010-06-09
*	Document grammar.cma->unix.cma dependency in CHANGES	glondu	2010-06-07
*	Added command "Locate Ltac qid".	herbelin	2010-06-03
*	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier	2010-06-03
*	Missing warning flush in a lexer message + update of CHANGES	herbelin	2010-05-12
*	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin	2010-04-22
*	A pass on the CHANGES file + credits for 8.3 (completing commit 12906	herbelin	2010-04-17
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)	herbelin	2010-03-28
*	Updated CHANGES wrt 8.3	herbelin	2010-03-23
*	Added automatic expansion on the left of recursive notations	herbelin	2010-03-23
*	update CHANGES : ocamlbuild, Structures, Numbers, MSets ... (cf. commit 8.3 r...	letouzey	2010-02-14
*	Documentation of the ! annotation for functor application	letouzey	2010-02-11
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau	2010-01-30
*	New command Declare Reduction <id> := <conv_expr>.	letouzey	2010-01-28
*	Document Local Declare ML Module	glondu	2010-01-14