coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-21
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\| \|\
\| * \|	More standard naming for the Imparg.with_implicits function.	Pierre-Marie Pédrot	2016-08-20
\| * \|	Fixing a bug in the presence of let-in while inferring the return clause.	Hugo Herbelin	2016-08-20
\| \| *	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
\| * \|	Test file for bug #4187.	Pierre-Marie Pédrot	2016-08-19
\| * \|	Fix performance bug: do not compute implicits of abstracted lemmas.	Pierre-Marie Pédrot	2016-08-19
\| * \|	Removing dead code in Impargs.	Pierre-Marie Pédrot	2016-08-19
\| * \|	Merge remote-tracking branch 'origin/pr/246' into v8.6	Matthieu Sozeau	2016-08-19
\| \|\ \
\| * \| \|	Moving Taccoerce to ltac/ folder.	Pierre-Marie Pédrot	2016-08-19
\| \| \| *	Remove extraneous dot in error message (bug #4832).	Guillaume Melquiond	2016-08-19
\| * \| \|	Fix anomaly on user-inputted projection name (bug #5029).	Guillaume Melquiond	2016-08-19
\| * \| \|	Merge remote-tracking branch 'github/bug4978' into v8.6	Matthieu Sozeau	2016-08-18
\| \|\ \ \
\| * \ \ \	Merge remote-tracking branch 'github/bug4188' into v8.6	Matthieu Sozeau	2016-08-18
\| \|\ \ \ \
\| \| \| \| \| *	Fix incorrect glob data for module symbols (bug #2336).	Guillaume Melquiond	2016-08-18
\| * \| \| \| \|	Fix an occurrence of deprecated eqn syntax in stdlib.	Maxime Dénès	2016-08-18
\| * \| \| \| \|	Fix bug #4939: LtacProf prints tactic notations weirdly.	Pierre-Marie Pédrot	2016-08-18
\| * \| \| \| \|	Adding a test for bug #4653.	Pierre-Marie Pédrot	2016-08-18
\| * \| \| \| \|	Merge PR #256 into v8.6	Pierre-Marie Pédrot	2016-08-18
\| \|\ \ \ \ \
\| \| * \| \| \| \|	In docs, fix command to reset Ltac profiling	Paul Steckler	2016-08-17
\| \|/ / / / /
\| \| * \| \| \|	Fix setoid_rewrite to raise proper errors	Matthieu Sozeau	2016-08-17
\| \| \| \| \| *	Fixing #5001 (metas not cleaned properly in clenv_refine_in).	Hugo Herbelin	2016-08-17
\| \| \| \| \| *	Fixing CHANGES.	Hugo Herbelin	2016-08-17
\| * \| \| \| \|	Documenting fix of #3070 (subst and chain of dependencies).	Hugo Herbelin	2016-08-17
\| \|/ / / /
* \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-17
\|\\| \| \| \|
* \| \| \| \|	Revert "CLEANUP: removing the definition of the "Context.Rel.Declaration.to_t...	Pierre-Marie Pédrot	2016-08-17
\| \| * \| \|	Fix #4978: priorities of Equivalence instances	Matthieu Sozeau	2016-08-17
\| \|/ / /
\| * \| \|	Fixing #3070 ("subst" taking properly into account chains of dependencies).	Hugo Herbelin	2016-08-17
\| * \| \|	Two protections against failures when printing evar_map.	Hugo Herbelin	2016-08-17
\| * \| \|	Fixing printing in debugger (no global env in debugger).	Hugo Herbelin	2016-08-17
\| * \| \|	A fix to dev/include.	Hugo Herbelin	2016-08-17
\| \| \| *	infoH: output via msg_* to make the XML protocol happy	Enrico Tassi	2016-08-17
\| * \| \|	Removing dead unsafe debugging code in Constrintern.	Pierre-Marie Pédrot	2016-08-16
\| \| \| *	Output a break before a list only if there was an empty line (bug #4606).	Guillaume Melquiond	2016-08-16
\| * \| \|	Merge PR #250 into v8.6	Pierre-Marie Pédrot	2016-08-16
\| \|\ \ \
\| * \ \ \	Merge PR #237 into v8.6	Pierre-Marie Pédrot	2016-08-16
\| \|\ \ \ \
\| * \ \ \ \	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\| \|\ \ \ \ \ \| \| \| \|_\|_\|/ \| \| \|/\| \| \|
\| * \| \| \| \|	Efficiently generate the pretyping contexts.	Pierre-Marie Pédrot	2016-08-16
\| \|\ \ \ \ \
\| \| \| * \ \ \	Merge branch 'pr255' into v8.5 (bug #5015)	Guillaume Melquiond	2016-08-16
\| \| \| \|\ \ \ \
\| \| \| \| * \| \| \|	Fix regression in Coqide's "forward one command" command	Xavier Leroy	2016-08-14
\| \| \| \|/ / / /
* \| \| \| \| \| \|	Adding "Context.Named.Declaraton.of_rel" function	Matej Kosik	2016-08-11
* \| \| \| \| \| \|	CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" fu...	Matej Kosik	2016-08-11
* \| \| \| \| \| \|	CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" fu...	Matej Kosik	2016-08-11
* \| \| \| \| \| \|	CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function	Matej Kosik	2016-08-11
* \| \| \| \| \| \|	CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function	Matej Kosik	2016-08-11
* \| \| \| \| \| \|	CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function	Matej Kosik	2016-08-11
\| \| \| * \| \| \|	Do not assume the "TERM" environment variable is always set (bug #5007).	Guillaume Melquiond	2016-08-11
\| \| \| * \| \| \|	Use the "md5" command on OpenBSD (bug #5008).	Guillaume Melquiond	2016-08-11
\| * \| \| \| \| \|	Make code a bit clearer by removing optional argument.	Guillaume Melquiond	2016-08-10
\| * \| \| \| \| \|	Remove unused optional "predicative" argument.	Guillaume Melquiond	2016-08-10