coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Reverting the following block of three commits:	Hugo Herbelin	2014-11-27
*	Registering strict implicit arguments systematically.	Hugo Herbelin	2014-11-26
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	Parsing and printing of primitive projections, fix buggy behavior when	Matthieu Sozeau	2014-09-10
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	- Fix the de Bruijn problem in check_projection for good :)	Matthieu Sozeau	2014-06-17
*	Fix printing of projections with implicits.	Matthieu Sozeau	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fix Bug 3217	Pierre Boutillier	2014-04-02
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (library)	ppedrot	2012-11-22
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	More comments and less doublons in some mli	pboutill	2011-02-10
*	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
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Continuing r12485-12486 (cleaning around name generation)	herbelin	2009-12-01
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Local/Global revision 12418 continued	herbelin	2009-10-26