coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-08
\|\
\| *	w_merge: Add a comment about the (List.rev evars)	Matthieu Sozeau	2016-10-06
\| *	unification.ml: fix for bug #4763, unif regression	Matthieu Sozeau	2016-10-06
* \|	Merge remote-tracking branch 'github/pr/263' into v8.6	Maxime Dénès	2016-10-03
\|\ \
* \ \	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-23
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fixing #5095 (non relevant too strict test in let-in abstraction).	Hugo Herbelin	2016-09-22
* \| \|	no-refold patch	Paul Steckler	2016-09-09
\| \| *	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
\| \|/ \|/\|
* \|	Pushing error backtrace in unification reraise.	Pierre-Marie Pédrot	2016-08-22
* \|	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
* \|	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