coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	Fix program using an the unsubstituted type of the original obligation	Matthieu Sozeau	2014-08-14
*	- Fix bug introduced in obligations which wouldn't consider all evars that are	Matthieu Sozeau	2014-07-16
*	Better handling of the universe context in case of Admitted proof obligations.	Matthieu Sozeau	2014-07-10
*	When defining a monomorphic Program, do not allow arbitrary instantiations	Matthieu Sozeau	2014-07-03
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Safer entry point of primitive projections in the kernel, now it does recognize	Matthieu Sozeau	2014-06-17
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	Enforce a correct exception handling in declaration_hooks	Enrico Tassi	2014-06-08
*	- Force every universe level to be >= Prop, so one cannot "go under" it anymore.	Matthieu Sozeau	2014-06-04
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06