coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Export definition of type implicits_list for contribs + fixed a	herbelin	2010-10-05
*	Fixing bugs in previous commits about implicit arguments:	herbelin	2010-10-04
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Dead code in impargs (afaics, no more need, since r11242, to merge	herbelin	2010-10-03
*	Fix function applications without labels (OCaml warning 6)	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Fixing bugs #2347 (part 2) and #2388: error message printing was done	herbelin	2010-09-18
*	* removed declare_constant and declare_internal_constant	vsiles	2010-09-02
*	* library/Library: Reformulate a comment.	regisgia	2010-08-27
*	* library/Library: Document.	regisgia	2010-08-27
*	* lib/Flags: Replace dont_load_proofs by load_proofs since not loading	regisgia	2010-08-27
*	* Improve documentation of LightenLibrary.	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing: New LightenLibrary.	regisgia	2010-08-27
*	* library/Library: Remove the use of the old-fashioned lighten_library.	regisgia	2010-08-27
*	* library/Library: Remove lighten_library definition.	regisgia	2010-08-27
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Some fine-tuning after removal of automatic imports of coercions in r13310	herbelin	2010-07-23
*	change the flag "internal" in declare/ind_tables from bool to	vsiles	2010-06-29
*	Moved error when option does not exist into a warning (this allows to	herbelin	2010-06-25
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Protection against anomaly when loading a state with bad magic number.	herbelin	2010-06-22
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Added command "Locate Ltac qid".	herbelin	2010-06-03
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Patch bug 2313.	soubiran	2010-05-05
*	"make source-doc" builds documentation of mli in html and pdf at	pboutill	2010-04-29
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Added a new exception for already declared Schemes,	vsiles	2010-04-27
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Granting wish #2249 (checking existing lemma name also when in a section).	herbelin	2010-04-09
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Simplify backtracking	vgross	2010-02-12
*	Fixing closing of segments.	vgross	2010-02-12
*	Small fix on module inclusion.	soubiran	2010-02-02
*	Various bug fix on recent features of the module system:	soubiran	2010-01-19
*	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
*	Declaremods.ml: a useless function wrongly introduced in last commit	letouzey	2009-12-08
*	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey	2009-12-07
*	declaremods.ml <--- code factoring	soubiran	2009-12-03
*	Continuing r12485-12486 (cleaning around name generation)	herbelin	2009-12-01
*	Now "Include Self <expr>" handles partially applied functors, cf for example ...	soubiran	2009-11-18
*	Module subtyping : allow many <: and module type declaration with <:	letouzey	2009-11-18
*	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey	2009-11-16
*	Include Self (Type) Foo: applying a (Type) Functor to the current context	letouzey	2009-11-16
*	Fixed bug #2168 (closing a section may have as side-effect the erasure	herbelin	2009-11-11
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08