coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Rename mkR* smart constructors (mostly in funind)	glondu	2010-12-25
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Fix diagram in genarg.mli	glondu	2010-12-23
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Prepare change of nomenclature rawconstr -> glob_constr	glondu	2010-12-23
*	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin	2010-12-04
*	Fixing several bugs with links to notation in coqdoc, including bug #2445:	herbelin	2010-12-04
*	Add information of localisation when an error involving an "implicit	herbelin	2010-11-07
*	Fixing a regression wrt 8.2 when using an "ident" several times in a notation	herbelin	2010-11-04
*	Move stuff about positive into a distinct PArith subdir	letouzey	2010-11-02
*	Cleaning the use of parentheses around evd and evdref (cosmetic commit).	herbelin	2010-10-31
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Fix function applications without labels (OCaml warning 6)	glondu	2010-09-28
*	Partial review of removed dead code (r13460)	herbelin	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	Bugfix: A notation for a constructor where some arguments are _	pboutill	2010-09-10
*	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin	2010-07-29
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22
*	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin	2010-07-22
*	Constrintern: Moved section about binders before section about notation	herbelin	2010-07-22
*	Switch to American spelling for "internalise" and "internalisation"	herbelin	2010-07-22
*	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau	2010-06-30
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin	2010-06-14
*	Fixing bug 2295 (omission of option "as" in return clause of "match" was not	herbelin	2010-06-13
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Fix bug #2262: bad implicit argument number by avoiding counting	msozeau	2010-06-09
*	Fixed wrong spelling in a warning.	herbelin	2010-06-08
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	Fix bug 2307	pboutill	2010-05-20
*	Nicer representation of tokens, more independant of camlp*	letouzey	2010-05-19
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Removed obsolete v7->v8 translation code (function check_same_type is	herbelin	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Fixed some printing bugs.	herbelin	2010-04-18
*	Optimized need for delimiters when disjoint scopes for strings and	herbelin	2010-04-10
*	Partially fixed bug #2231 (an inductive parameter name was internally	herbelin	2010-04-10
*	Improving compatibility between 8.2 and 8.3	herbelin	2010-04-05
*	Small things about coqdoc + fixing lettuple.v test (part of bug #2289)	herbelin	2010-03-30
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Fix implicit_application for let-bound variables in the class context.	msozeau	2010-01-28
*	Backport fixes in Instance declarations to Program Instance.	msozeau	2010-01-28
*	Variant !F M for functor application that does not honor the Inline declarations	letouzey	2010-01-17
*	Include can accept both Module and Module Type	letouzey	2010-01-07