coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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 enforcing that module types have no retroknowledge.	Pierre-Marie Pédrot	2017-08-29
*	Separating the module_type and module_body types by using a type parameter.	Pierre-Marie Pédrot	2017-08-29
*	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
*	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-24
\|\
\| *	Making the side_effects type opaque.	Pierre-Marie Pédrot	2017-03-23
* \|	[toplevel] Remove unusable option -notop	Emilio Jesus Gallego Arias	2017-03-14
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-01
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2017-02-01
\| \|\
\| \| *	[native comp] Improve error message on linking error.	Emilio Jesus Gallego Arias	2017-01-26
\| * \|	Do not add redundant side effects in tactic code.	Pierre-Marie Pédrot	2017-01-20
\| \| *	Fix for bug #4863, update the Proofview's env with	Matthieu Sozeau	2016-10-11
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
* \| \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| \|/ / \|/\| \|
\| * \|	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
\|/ /
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\\|
\| *	Prevent unsafe overwriting of Required modules by toplevel library.	Maxime Dénès	2016-07-05
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	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
\| \| *	Hashconsing modules.	Pierre-Marie Pédrot	2016-03-10
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \|
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\| \|
\| * \|	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
* \| \|	Hashconsing modules.	Pierre-Marie Pédrot	2015-11-15
\|/ /
* \|	Collect subproof universes in handle_side_effects.	Matthieu Sozeau	2015-10-29
* \|	Cleanup API and comments of 908dcd613	Enrico Tassi	2015-10-29
* \|	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
* \|	Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)	Pierre Letouzey	2015-10-25
* \|	Minor module cleanup : error HigherOrderInclude was never happening	Pierre Letouzey	2015-10-25
* \|	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
* \|	Univs: handle side-effects of futures correctly in kernel.	Matthieu Sozeau	2015-10-02
* \|	Univs: module constraints move to universe contexts as they might	Matthieu Sozeau	2015-10-02
\| *	Propagate `Guarded` flag from syntax to kernel.	Arnaud Spiwack	2015-09-25