coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
*	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
*	CLEANUP: in the Reductionops module	Matej Kosik	2015-12-17
*	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
*	Fixing unexpected length of context in a typing function, detected by	Hugo Herbelin	2015-12-15
*	Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.	Hugo Herbelin	2015-12-15
*	API: documenting context_chop and removing a duplicate.	Hugo Herbelin	2015-12-15
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\
\| *	Optimize occur_evar_upto_types, avoiding repeateadly looking into the	Matthieu Sozeau	2015-12-11
* \|	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05
* \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \|	Simplifying an instantiation function using subst_of_rel_context_instance.	Hugo Herbelin	2015-12-05
* \|	About building of substitutions from instances.	Hugo Herbelin	2015-12-05
* \|	An example in centralizing similar functions to a common place so that	Hugo Herbelin	2015-12-05
* \|	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