coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	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
*	Add the possibility of defining opaque terms with program.	mlasson	2015-01-21
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Tentatively more informative report of failure when inferring	Hugo Herbelin	2014-12-11
*	Exporting the function handling side-effects only applied to terms.	Pierre-Marie Pédrot	2014-11-20
*	Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.	Arnaud Spiwack	2014-10-22
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	Merging some functions from evarutil.ml/evd.ml.	Hugo Herbelin	2014-09-29
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30