coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	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-04-02	Fix Bug 3217	Pierre Boutillier
2014-03-01	Fixing pervasive comparisons	Pierre-Marie Pédrot
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-04-22	code simplifications concerning Summary	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey
2013-01-28	Actually adding backtrace handling.	ppedrot
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-11-22	Monomorphization (library)	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	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-08-08	Updating headers.	herbelin
2012-05-29	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-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin
2012-03-02	Noise for nothing	pboutill
2011-12-18	Fixed a Not_found bug when declaring in a section some implicit	herbelin
2011-12-06	Minor fixes to Arguments	gareuselesinge
2011-11-21	Renamig support added to "Arguments"	gareuselesinge
2011-11-21	New Arguments vernacular	gareuselesinge
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-02-10	More comments and less doublons in some mli	pboutill
2010-10-05	Export definition of type implicits_list for contribs + fixed a	herbelin
2010-10-04	Fixing bugs in previous commits about implicit arguments:	herbelin
2010-10-03	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-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-16	Util: remove list_split_at which is a clone of list_chop	letouzey
2009-12-01	Continuing r12485-12486 (cleaning around name generation)	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-10-26	Local/Global revision 12418 continued	herbelin
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Remove useless Liboject.export_function field	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-13	Death of "survive_module" and "survive_section" (the first one was	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-06-01	Prevent automatic inference of implicit arguments when the auto flag is	msozeau