coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A mini-optimization for free in unification.ml: test in O(1)	Hugo Herbelin	2016-06-10
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot	2016-03-20
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-20
\|\
\| *	Fix #4623: set tactic too weak with universes (regression)	Maxime Dénès	2016-03-17
\| *	Try eta-expansion of records only on non-recursive ones	Matthieu Sozeau	2016-03-15
* \|	Try eta-expansion of records only on non-recursive ones	Matthieu Sozeau	2016-03-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\\|
\| *	Fix strategy of Keyed Unification	Matthieu Sozeau	2016-03-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
\| *	Fix part of bug #4533: respect declared global transparency of	Matthieu Sozeau	2016-02-23
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \| \| \|/ \| \|/\|
\| \| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ \|/\|
\| *	Optimizing the computation of frozen evars.	Pierre-Marie Pédrot	2016-02-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Extend last commit: keyed unification uses full conversions on the applied co...	Matthieu Sozeau	2016-01-12
\| *	Fix essential bug in new Keyed Unification mode reported by R. Krebbers.	Matthieu Sozeau	2016-01-12
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	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
* \|	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
* \|	More monotonicity in Tactics.	Pierre-Marie Pédrot	2015-10-19
* \|	Making Evarutil.new_evar monotonous.	Pierre-Marie Pédrot	2015-10-18
* \|	Removing subst_defined_metas_evars from Evd.	Pierre-Marie Pédrot	2015-09-27
\|/
*	Refining 71def2f8 on too strong occur-check limiting evar-evar	Hugo Herbelin	2015-07-16
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.	Hugo Herbelin	2015-02-23
*	Fixing occur-check which was too strong in unification.ml.	Hugo Herbelin	2015-02-23
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Simplifying second_order_matching: no need to invert the linear	Hugo Herbelin	2014-12-30
*	New try on Fixing an evar_map bug revealed by commit 603b66f81 on	Hugo Herbelin	2014-12-15
*	Documenting check_record + changing a possibly undefined int into int option.	Hugo Herbelin	2014-12-15
*	Two fixes in unification (bugs #3782 and #3709)	Matthieu Sozeau	2014-12-12
*	Commit not ready. Sorry.	Hugo Herbelin	2014-12-11
*	Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.	Hugo Herbelin	2014-12-11
*	Fix debugger Tactic Unification.	Hugo Herbelin	2014-12-05
*	Small cleaning and uniformization in unification flags:	Hugo Herbelin	2014-12-05
*	Reverting the following block of three commits:	Hugo Herbelin	2014-11-27
*	Fixing Coq compilation.	Pierre-Marie Pédrot	2014-11-26
*	Experimenting always forcing convertibility on strict implicit arguments	Hugo Herbelin	2014-11-26
*	A bit more information in debug tactic unification.	Hugo Herbelin	2014-11-25
*	Experimenting using unification when matching evar/meta free subterms	Hugo Herbelin	2014-11-25
*	Option -type-in-type continued (deactivate test for inferred sort of	Hugo Herbelin	2014-11-19
*	Accepting conversion on inner closed subterms while looking for	Hugo Herbelin	2014-11-11