coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-18
\|\
\| *	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
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\| \|
\| * \|	Completing reverting generalization and cleaning of the return clause inference.	Hugo Herbelin	2016-10-13
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\| \|
\| * \|	Reverting generalization and cleaning of the return clause inference in v8.6.	Hugo Herbelin	2016-10-11
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\| \|
\| * \|	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
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\| \|
\| * \|	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
\| \|\ \
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\| \| \|
\| * \| \|	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
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-27
\|\\| \| \|
\| * \| \|	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.6'	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
* \| \| \|	Make the Coq codebase independent from Ltac-related code.	Pierre-Marie Pédrot	2016-09-16
\|\ \ \ \
\| * \| \| \|	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
* \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\ \ \ \ \ \| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	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
* \| \| \| \| \|	Propagate location info on pattern match compilation.	Emilio Jesus Gallego Arias	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
\| \| \|_\|/ \| \|/\| \|
\| \| \| *	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot	2016-09-08
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
* \| \| \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
* \| \| \|	CLEANUP: using \|> operator more consistently	Matej Kosik	2016-08-30
* \| \| \|	CLEANUP: taking advantage of "_ % _" operator to express function composition...	Matej Kosik	2016-08-29
* \| \| \|	CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...	Matej Kosik	2016-08-26
* \| \| \|	Merge remote-tracking branch 'v8.6' into trunk	Matej Kosik	2016-08-25
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
* \| \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24