coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Extraction: Richer patterns in matchs as proposed by P.N. Tollitte	letouzey	2011-11-28
*	Extraction: in haskell, __ may have any type, no need to unsafeCoerce it	letouzey	2011-07-04
*	Extraction: unfolds the let-in created by Program when handling "match"	letouzey	2011-04-07
*	Extraction: avoid some useless Obj.magic by fixing my ML type unifier	letouzey	2011-04-07
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey	2010-12-21
*	Dead code in extraction	letouzey	2010-09-24
*	Extraction: multiple fixes related with the Not_found encountered by X. Leroy	letouzey	2010-09-17
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extraction: restrict autoinling to csts whose body is globally visible (fix #...	letouzey	2010-07-08
*	Extraction: more factorization of common match branches	letouzey	2010-07-08
*	Extraction: Unset Extraction AutoInline is now the default	letouzey	2010-07-08