coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| *	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
* \| \| \|	CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function	Matej Kosik	2016-08-24
* \| \| \|	CLEANUP: removing superfluous (module) qualifiers	Matej Kosik	2016-08-24
* \| \| \|	Changing the definition of the "Lib.variable.info" type to enable us to do mo...	Matej Kosik	2016-08-24
\| * \| \|	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
\| \| * \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| \| * \|	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\| \| * \|	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\| \|/ / \|/\| \|
\| * \|	[pp] Fix newline issues.	Emilio Jesus Gallego Arias	2016-08-19
\|/ /
* \|	Two protections against failures when printing evar_map.	Hugo Herbelin	2016-08-17