coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
*	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Merge PR #1118: Extraction : minor support stuff for the new Extraction Compu...	Maxime Dénès	2017-10-06
\|\
* \|	Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...	Pierre Letouzey	2017-10-05
\| *	Extraction : minor support stuff for the new Extraction Compute plugin	Pierre Letouzey	2017-10-04
\|/
*	Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...	Pierre Letouzey	2017-07-25
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Extraction: slightly better heuristic for Obj.magic simplifications	Pierre Letouzey	2015-12-16
*	Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplifications	Pierre Letouzey	2015-12-16
*	Extraction: fix a few little glitches with my last commit (replacing unused v...	Pierre Letouzey	2015-12-15
*	Extraction: replace unused variable names by _ in funs and matchs (fix #2842)	Pierre Letouzey	2015-12-15
*	Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)	Pierre Letouzey	2015-12-14
*	Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)	Pierre Letouzey	2015-12-14
*	Extraction: nicer implementation of Implicits	Pierre Letouzey	2015-12-12
*	Fix some typos.	Guillaume Melquiond	2015-10-13
*	Update headers.	Maxime Dénès	2015-01-12
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Fixing Pervasives.equality in extraction.	Pierre-Marie Pédrot	2014-03-03
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Nicer code concerning dirpaths and modpath around Lib	letouzey	2013-08-22
*	Restrict (try...with...) to avoid catching critical exn (part 6)	letouzey	2013-03-13
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Names: shortcuts for building {kn, constant, mind} with empty sections	letouzey	2013-02-26
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
*	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
*	Add option Set/Unset Extraction Conservative Types.	aspiwack	2012-08-24
*	Updating headers.	herbelin	2012-08-08
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Extraction: only do the test on generalizable lets for ocaml	letouzey	2011-12-10
*	Extraction: avoid internal eta-reduction (fix #2570)	letouzey	2011-12-08
*	Extraction: typo in last commit	letouzey	2011-11-29