coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \|	Leveraging GADTs to provide a better Dyn API.	Pierre-Marie Pédrot	2015-12-05
\|/
*	Declaremods: replace two anomalies by user errors (fix #3974 and #3975)	Pierre Letouzey	2015-10-25
*	Native compiler: refactor code handling pre-computed values.	Maxime Dénès	2015-07-10
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Partially revert "Forbid Require inside interactive modules and module types."	Maxime Dénès	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	Forbid Require inside interactive modules and module types.	Maxime Dénès	2014-12-25
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	selective join/export of the safe_environment	Enrico Tassi	2014-10-13
*	Fix Declaremods.end_library (Closes: #3536)	Enrico Tassi	2014-09-02
*	Fixing ml-doc.	Pierre-Marie Pédrot	2014-05-01
*	STM: make -async-proofs on work from coqc too	Enrico Tassi	2014-03-18
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot	2013-11-22
*	Nicer code concerning dirpaths and modpath around Lib	letouzey	2013-08-22
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Safe_typing code refactoring	letouzey	2013-08-20
*	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge	2013-08-08
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	Modops.destr_functor without useless env	letouzey	2013-07-17
*	Lib.contents () instead of Lib.contents_after None	letouzey	2013-07-17
*	More dynamic argument scopes	letouzey	2013-07-17
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Fix issues with "Reset Initial" in scripts given to coqtop -l	letouzey	2013-04-23
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Declaremods: some more minor cleanup	letouzey	2013-04-22
*	Minor simplifications in Declaremods and Safe_typing	letouzey	2013-04-15
*	Declaremods: drop some useless stuff (slight gain in vo size)	letouzey	2013-04-15
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Declaremods: a few syntactic improvements	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Actually adding backtrace handling.	ppedrot	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of mod_bound_id	ppedrot	2012-12-18
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Stringset and Stringmap to String namespace.	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
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14