coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-18
\|\
* \|	Quick fix to unification regression #4955.	Hugo Herbelin	2016-10-17
\| *	Fixing to #3209 (Not_found due to an occur-check cycle).	Hugo Herbelin	2016-10-17
\| *	Fixing a missing constraint in consider_remaining_unif_constraints.	Hugo Herbelin	2016-10-17
* \|	Completing reverting generalization and cleaning of the return clause inference.	Hugo Herbelin	2016-10-13
* \|	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-08
\|\\|
* \|	Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.	Pierre-Marie Pédrot	2016-10-08
* \|	Fix bug #4464: "Anomaly: variable H' unbound. Please report.".	Pierre-Marie Pédrot	2016-10-07
\| *	evarconv.ml: Fix bug #4529, primproj unfolding	Matthieu Sozeau	2016-10-06
\| *	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
* \|	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
* \|	Merge remote-tracking branch 'github/pr/263' into v8.6	Maxime Dénès	2016-10-03
\|\ \
* \| \|	Fix bug #4723 and FIXME in API for solve_by_tac	Matthieu Sozeau	2016-09-28
* \| \|	Remove incorrect assertion in cbn (bug #4822).	Guillaume Melquiond	2016-09-28
* \| \|	Posssible abstractions over goal variables when inferring match return clause.	Hugo Herbelin	2016-09-26
* \| \|	Trying an abstracting dependencies heuristic for the match return clause even...	Hugo Herbelin	2016-09-26
* \| \|	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin	2016-09-26
* \| \|	Inference of return clause: giving uniformly priority to "small inversion".	Hugo Herbelin	2016-09-26
* \| \|	Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].	Pierre-Marie Pédrot	2016-09-23
* \| \|	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
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\|\\| \|
* \| \|	Merge remote-tracking branch 'github-coq/pr/249' into v8.6	Matthieu Sozeau	2016-09-12
\|\ \ \
\| \| * \|	Fixing #5077 (failure on typing a fixpoint with evars in its type).	Hugo Herbelin	2016-09-10
\| * \| \|	no-refold patch	Paul Steckler	2016-09-09
* \| \| \|	Fast path in Clenvtac.clenv_refine typeclass resolution.	Pierre-Marie Pédrot	2016-09-09
* \| \| \|	Monomorphize a costly boolean equality operation.	Pierre-Marie Pédrot	2016-09-09
\|/ / /
\| \| *	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
\| \|/ \|/\|
* \|	Merge PR #258: "Fix newline issues" into v8.6	Pierre-Marie Pédrot	2016-08-24
\|\ \
* \| \|	Pushing error backtrace in unification reraise.	Pierre-Marie Pédrot	2016-08-22
* \| \|	Do not recompute the whole evar naming environment in GProd intepretation.	Pierre-Marie Pédrot	2016-08-21
* \| \|	Short path for Pretyping.ltac_interp_name_env.	Pierre-Marie Pédrot	2016-08-21
* \| \|	Fixing a bug in the presence of let-in while inferring the return clause.	Hugo Herbelin	2016-08-20
\| * \|	[pp] Fix newline issues.	Emilio Jesus Gallego Arias	2016-08-19
\|/ /
* \|	Two protections against failures when printing evar_map.	Hugo Herbelin	2016-08-17
* \|	Efficiently generate the pretyping contexts.	Pierre-Marie Pédrot	2016-08-16
\|\ \
* \| \|	Make it a bit more obvious when variables are of type unit.	Guillaume Melquiond	2016-08-10
\| * \|	Using a dedicated kind of substitutions in evar name generation.	Pierre-Marie Pédrot	2016-08-06
\| * \|	Using the extended contexts in pretyping.	Pierre-Marie Pédrot	2016-08-05
\| * \|	Embedding the pretyping environment in a dummy record.	Pierre-Marie Pédrot	2016-08-04
\|/ /
* \|	A new step on using alpha-conversion in printing notations.	Hugo Herbelin	2016-07-18
* \|	Partial fix to #4592 (notation requiring alpha-conversion for printing).	Hugo Herbelin	2016-07-17
* \|	Remove spurious warnings about projections when requiring modules.	Pierre-Marie Pédrot	2016-07-08
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\\|
* \|	Merge remote-tracking branch 'github/bug4653' into v8.6	Matthieu Sozeau	2016-07-07
\|\ \
* \| \|	Fix reopened bug #3317.	Matthieu Sozeau	2016-07-06
* \| \|	Disallow dependent case on prim records w/o eta	Matthieu Sozeau	2016-07-06
* \| \|	Renaming to more generic has_dependent_elim test	Matthieu Sozeau	2016-07-06