coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Extraction: msg_notice instead of msg_info.	Pierre Courtieu	2016-01-04
*	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
*	Extraction: cosmetically avoid generating spaces on empty lines	Pierre Letouzey	2015-12-14
*	Extraction: nicer implementation of Implicits	Pierre Letouzey	2015-12-12
*	Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)	Pierre Letouzey	2015-12-12
*	Add extraction to JSON.	Nickolai Zeldovich	2015-04-09
*	Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)	Guillaume Melquiond	2015-03-21
*	Univs: fix bug #3978: carry around the universe context used to	Matthieu Sozeau	2015-02-12
*	Update headers.	Maxime Dénès	2015-01-12
*	Extraction: discard code unnecessary to fulfill a module signature	Pierre Letouzey	2015-01-11
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	Extraction: discard unnecessary code inside modules without signatures	Pierre Letouzey	2015-01-11
*	Extraction : some more support functions for a future "Extraction Compute"	Pierre Letouzey	2015-01-11
*	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
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Nicer code concerning dirpaths and modpath around Lib	letouzey	2013-08-22
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Lib.contents () instead of Lib.contents_after None	letouzey	2013-07-17
*	Extraction : message about lack of support for toplevel Include	letouzey	2013-07-17
*	Extract_env : correct exceptions mentionned in a try ... with	letouzey	2013-03-15
*	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey	2013-03-13
*	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
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Extraction: avoid initial strange empty comments after Arnaud's hack	letouzey	2012-10-30
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	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
*	Experimental support for a comment in the files' preamble in extraction.	aspiwack	2012-08-24
*	Updating headers.	herbelin	2012-08-08
*	Vecnacentries.dump_global silently ignores exceptions	pboutill	2012-08-06
*	Dump references in Extraction	pboutill	2012-08-05
*	More cleaning	ppedrot	2012-06-01
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Module names and constant/inductive names are now in two separate namespaces	letouzey	2012-03-26
*	Noise for nothing	pboutill	2012-03-02
*	Extract_env: generic = on prec_declaration replaced by prec_declaration_equal	puech	2011-07-29