coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias	2017-02-15
*	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
*	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
*	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
*	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
\| *	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	Program: fix #4873: transparency option not used	Matthieu Sozeau	2016-07-07
*	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	Pierre Letouzey	2016-07-03
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Program: refine shrinking of obligations	Matthieu Sozeau	2016-06-27
*	Rework treatment of default transparency of obligations	Matthieu Sozeau	2016-06-27
*	Shrink Proofs/Obligations by default and deprecate	Matthieu Sozeau	2016-06-27
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\
* \|	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
* \|	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
* \|	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\ \
\| * \|	Allow `Pretyping.search_guard` to not check guard	Arnaud Spiwack	2016-06-15
* \| \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| \| *	Program: remove debug tracing	Matthieu Sozeau	2016-05-26
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fix bug #3887: Better error message for "More than one program with unsolved ...	Pierre-Marie Pédrot	2016-05-09
* \| \|	Moving the use of Tactic_option from Obligations to G_obligations.	Pierre-Marie Pédrot	2016-03-19
* \| \|	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-29
\|\\| \|
\| * \|	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
* \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \
\| * \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\|/ / /
* \| \|	Moving three related small half-general half-ad-hoc utility functions	Hugo Herbelin	2015-12-05
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\| \|
\| * \|	Univs/Program: update the universe context with global universe	Matthieu Sozeau	2015-12-02
\| * \|	Fix bug #4444: Next Obligation performed after a Section opening was	Matthieu Sozeau	2015-12-02
* \| \|	Removing dead code in Obligations.	Pierre-Marie Pédrot	2015-12-02
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\| \|
\| * \|	Univs: carry on universe substitution when defining obligations of	Matthieu Sozeau	2015-11-24
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\| \|
\| * \|	Allow program hooks to see the refined universe_context at the end of a	Matthieu Sozeau	2015-11-19
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\| \|
\| * \|	Add a way to get the right fix_exn in external vernacular commands	Matthieu Sozeau	2015-10-30
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\| \|
\| * \|	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\| \|
\| * \|	Fix Next Obligation to not raise an anomaly in case of mutual	Matthieu Sozeau	2015-10-09