coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\| \|
\| * \|	Univs: fix FingerTree contrib.	Matthieu Sozeau	2015-10-07
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\| \|
\| * \|	Univs/program: handle side effects in obligations.	Matthieu Sozeau	2015-10-02
\| * \|	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
* \| \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\| \|
\| * \|	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
* \| \|	All Program obligations now respect the Shrink Obligation flag.	Pierre-Marie Pédrot	2015-09-08
* \| \|	Fixing the Shrink Obligations option.	Pierre-Marie Pédrot	2015-09-08
\|/ /
* /	Code cleaning in Obligations.	Pierre-Marie Pédrot	2015-08-22
\|/
*	obligations: wrap Ephemeron.get to make error more informative	Enrico Tassi	2015-06-23
*	Wrap the program_info type up in the ephemeron mechanism	Alec Faithfull	2015-06-23
*	Program: Do not reduce obligation types preemptively, only at	Matthieu Sozeau	2015-04-13