coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing dynamic inclusion of constrs in tactic AST.	Pierre-Marie Pédrot	2015-12-04
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\
\| *	Add an option to deactivate compatibility printing of primitive	Matthieu Sozeau	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
* \|	More efficient implementation of equality-up-to-universes in Universes.	Pierre-Marie Pédrot	2015-11-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\|
\| *	Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).	Hugo Herbelin	2015-11-25
\| *	Fixing an old typo in Retyping, found by Matej.	Hugo Herbelin	2015-11-24
\| *	Fixing a vm_compute bug in the presence of let-ins among the	Hugo Herbelin	2015-11-22
\| *	Fixing a bug of adjust_subst_to_rel_context.	Hugo Herbelin	2015-11-22
\| *	Fixing kernel bug in typing match with let-ins in the arity.	Hugo Herbelin	2015-11-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	Fix bug #4433, removing hack on evars appearing in a pattern from a	Matthieu Sozeau	2015-11-19
\| *	Performance fix for destruct.	Pierre-Marie Pédrot	2015-11-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	Ensure that conversion is called on terms of the same type in	Matthieu Sozeau	2015-11-11
\| *	Fix bug #3998: when using typeclass resolution for conversion, allow	Matthieu Sozeau	2015-11-11
\| *	Fix bug #4293: ensure let-ins do not contain algebraic universes in	Matthieu Sozeau	2015-11-11
* \|	Revert "Fixing #1225: we now skip the canonically built binding contexts of"	Hugo Herbelin	2015-11-10
* \|	Fixing #1225: we now skip the canonically built binding contexts of	Hugo Herbelin	2015-11-10
* \|	Merge origin/v8.5 into trunk	Hugo Herbelin	2015-11-10
\|\\|
\| *	Pushing the backtrace in conversion anomalies.	Pierre-Marie Pédrot	2015-11-09
* \|	Experimenting printing the type of the defined term of a LetIn when	Hugo Herbelin	2015-11-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Univs: missing checks in evarsolve with candidates and missing a	Matthieu Sozeau	2015-11-04
\| *	Univs: update refman, better printers for universe contexts.	Matthieu Sozeau	2015-11-04
\| *	Univs: compatibility with 8.4.	Matthieu Sozeau	2015-11-04
\| *	Fix bug #4151: discrepancy between exact and eexact/eassumption.	Matthieu Sozeau	2015-11-02
\| *	Refresh rigid universes as well, and in 8.4 compatibility mode,	Matthieu Sozeau	2015-11-02
\| *	Handle side-effects of Vernacular commands inside proofs better, so that	Matthieu Sozeau	2015-10-29
* \|	Removing some goal unsafeness in inductive schemes.	Pierre-Marie Pédrot	2015-10-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Univs: local names handling.	Matthieu Sozeau	2015-10-28
\| *	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
\| *	Fix bug in native compiler with universe polymorphism.	Maxime Dénès	2015-10-28
\| *	Refine Gregory Malecha's patch on VM and universe polymorphism.	Maxime Dénès	2015-10-28
\| *	Conversion of polymorphic inductive types was incomplete in VM and native.	Maxime Dénès	2015-10-28
\| *	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
\| *	Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"	Hugo Herbelin	2015-10-28
\| *	Documenting a bit more interpretation functions in passing.	Hugo Herbelin	2015-10-26
* \|	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