coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Let definitions do not create new universe constraints.	Pierre-Marie Pédrot	2017-12-19
*	Specific type for section definition entries.	Pierre-Marie Pédrot	2017-12-19
*	Let definitions must not contain side-effects when reaching the kernel.	Pierre-Marie Pédrot	2017-12-16
*	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	[stm] [flags] Move document mode flags to the STM.	Emilio Jesus Gallego Arias	2017-10-06
*	Statically ensuring that inlined entries out of the kernel have no effects.	Pierre-Marie Pédrot	2017-07-26
*	Further simplication: do not recreate entries for side-effects.	Pierre-Marie Pédrot	2017-07-26
*	Remove a horrendous hack in Declare to retrieve exported side-effects.	Pierre-Marie Pédrot	2017-07-26
*	More precise type of entries capturing their lack of side-effects.	Pierre-Marie Pédrot	2017-07-26
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Documenting the API of side-effects.	Pierre-Marie Pédrot	2017-03-23
*	Making the side_effects type opaque.	Pierre-Marie Pédrot	2017-03-23
*	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
* \|	Univs: Change intf of push_named_def to return the computed universe	Matthieu Sozeau	2015-10-02
* \|	Univs: refined handling of assumptions	Matthieu Sozeau	2015-10-02
\| *	Propagate `Guarded` flag from syntax to kernel.	Arnaud Spiwack	2015-09-25
* \|	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
* \|	Native compiler: refactor code handling pre-computed values.	Maxime Dénès	2015-07-10
\|/
*	Fix bug #4159	Matthieu Sozeau	2015-05-27
*	Update headers.	Maxime Dénès	2015-01-12
*	selective join/export of the safe_environment	Enrico Tassi	2014-10-13
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	.vi files: .vo files without proofs	Enrico Tassi	2014-01-04
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	Future: ported to Ephemeron + exception enhancing	gareuselesinge	2013-10-18
*	ind_tables: properly handling side effects	gareuselesinge	2013-08-30
*	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
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Added a Register Inline command for the native compiler. Will be ported to th...	mdenes	2013-07-10
*	Use definition_entry to declare local definitions	gareuselesinge	2013-05-09
*	Minor simplifications in Declaremods and Safe_typing	letouzey	2013-04-15
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Dir_path --> DirPath	letouzey	2013-02-19
*	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