coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\
\| *	Fix lemma-overloading	Matthieu Sozeau	2015-10-20
\| *	Do occur-check w.r.t existential's types also when instantiating an evar.	Matthieu Sozeau	2015-10-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
* \|	More monotonicity in Tactics.	Pierre-Marie Pédrot	2015-10-19
* \|	Making Evarutil.new_evar monotonous.	Pierre-Marie Pédrot	2015-10-18
\| *	Using "__" rather than this unelegant arbitrary "A" for the name of variables...	Hugo Herbelin	2015-10-18
\| *	Fixing #4198 (continued): not matching within the inner lambdas/let-ins	Hugo Herbelin	2015-10-18
\| *	Using appropriate lambda decomposition function counting let-ins when	Hugo Herbelin	2015-10-18
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-10-16
\|\\|
\| *	Avoid dependency of the pretyper on C code.	Maxime Dénès	2015-10-15
\| *	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
\| *	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Occur-check in evar_define was not strong enough.	Matthieu Sozeau	2015-10-14
\| *	Fix constr_matching when a match is found in the head of a case construct	Matthieu Sozeau	2015-10-14
\| *	Fixing evarmap implementation.	Pierre-Marie Pédrot	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-12
\|\\|
\| *	Fix rechecking of applications: it can be given ill-typed terms. Fixes math-c...	Matthieu Sozeau	2015-10-12
\| *	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
\| *	Refining 0c320e79ba30 in fixing interpretation of constr under binders	Hugo Herbelin	2015-10-11
\| *	Fixing obviously untested fold_glob_constr and iter_glob_constr.	Hugo Herbelin	2015-10-11
\| *	Constr_matching: renaming misleading name stk into ctx.	Hugo Herbelin	2015-10-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	Code cleaning in VM (with Benjamin).	Maxime Dénès	2015-10-09
\| *	Fix inference of return clause raising a type error.	Matthieu Sozeau	2015-10-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Univs: fix bug #3807	Matthieu Sozeau	2015-10-08
\| *	Univs: fix bug #4161.	Matthieu Sozeau	2015-10-08
\| *	Univs: fix FingerTree contrib.	Matthieu Sozeau	2015-10-07
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Univs (pretyping): call vm_compute/native_compute with the current	Matthieu Sozeau	2015-10-06
\| *	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	Univs: fix bug #4251, handling of template polymorphic constants.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
\| \| *	Univs (pretyping): allow parsing and decl of Top.n	Matthieu Sozeau	2015-10-02
\| \| *	Univs (evd): deal with global universes and sideff	Matthieu Sozeau	2015-10-02
\| \| *	Forcing i > Set for global universes (incomplete)	Matthieu Sozeau	2015-10-02
\| \| *	Univs: force all universes to be >= Set.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: Fix part of bug #4161	Matthieu Sozeau	2015-10-02
\| \| *	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
\| \|/
* \|	Removing subst_defined_metas_evars from Evd.	Pierre-Marie Pédrot	2015-09-27
\| *	Fixing loss of extra data in Evd.	Pierre-Marie Pédrot	2015-09-27
* \|	Hardening the API of evarmaps.	Pierre-Marie Pédrot	2015-09-26