coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-08-01
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[lib] Remove obsolete state-management function add_frozen_state	Emilio Jesus Gallego Arias	2017-06-12
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
*	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	LtacProf for Coq trunk	Jason Gross	2016-06-05
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\
\| *	Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.	Pierre-Marie Pédrot	2016-05-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	Fix bug #4292: Unexpected functor objects.	Pierre-Marie Pédrot	2016-05-03
* \|	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