coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
*	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias	2017-11-29
*	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	[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