coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Rely on kernel to know if a name is already used so as to be consistent with it.	herbelin	2011-10-08
*	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin	2011-10-05
*	Completing r14448 and thus continuing r14407 (using Cast to propagate	herbelin	2011-09-24
*	Hash-consing: attempt to stop hash-consing separately constr in declare.ml	letouzey	2011-09-22
*	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey	2011-09-15
*	Coqide: new backtracking code, based on the Backtrack command	letouzey	2011-09-05
*	Lib: remove strange code about backtracking to the current state	letouzey	2011-09-05
*	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey	2011-09-05
*	Heads: generic equality on constr replaced by destructor	puech	2011-07-29
*	Modops: the strengthening functions can work without any env argument	letouzey	2011-05-17
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Goptions: repair Unset for int options	letouzey	2011-03-17
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	Annotations at functor applications:	letouzey	2011-02-11
*	More comments and less doublons in some mli	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
*	Fix some typos	glondu	2011-01-11
*	Minor code improvements around libobject	herbelin	2010-10-31
*	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