coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Program: cleanup in cases, add options	Matthieu Sozeau	2016-06-29
*	Merge branch 'bug4527' into trunk	Matthieu Sozeau	2016-06-29
\|\
\| *	Univ: Use loc even if there are more unbound levels	Matthieu Sozeau	2016-06-29
\| *	CHANGES: document fix for #4726 too.	Matthieu Sozeau	2016-06-29
\| *	CHANGES: document fix for 4527 and compatibility.	Matthieu Sozeau	2016-06-29
\| *	universes.ml: Minor code cleanup	Matthieu Sozeau	2016-06-29
\| *	Univs: Fix bug #4726	Matthieu Sozeau	2016-06-29
\| *	Univs: add source locations of levels	Matthieu Sozeau	2016-06-29
\| *	Univs: earlier errors for strict univ decls #4527	Matthieu Sozeau	2016-06-29
\|/
*	Merge branch 'warnings' into trunk	Maxime Dénès	2016-06-29
\|\
\| *	Fix issues in test-suite revealed by warnings.	Maxime Dénès	2016-06-29
\| *	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
\| *	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-29
* \|	Revert "A new infrastructure for warnings."	Maxime Dénès	2016-06-28
* \|	Typeclasses: use once in by clause for typeclass eauto	Matthieu Sozeau	2016-06-28
* \|	Merge branch 'warnings' into trunk	Maxime Dénès	2016-06-28
\|\ \
\| * \|	A new infrastructure for warnings.	Maxime Dénès	2016-06-28
\|/ /
* \|	Merge remote-tracking branch 'github/pr/207' into trunk	Maxime Dénès	2016-06-28
\|\ \ \| \|/ \|/\|
* \|	Finalizing the only printing feature.	Pierre-Marie Pédrot	2016-06-28
\|\ \
\| * \|	Documenting the "only printing" notation flag.	Pierre-Marie Pédrot	2016-06-28
\| * \|	Adding a test-suite for the only printing flag.	Pierre-Marie Pédrot	2016-06-28
\| * \|	Properly handle the only printing flag in Reserved Notations.	Pierre-Marie Pédrot	2016-06-28
\| * \|	Properly handling the only printing flag when parsing rules already exist.	Pierre-Marie Pédrot	2016-06-28
\|/ /
* \|	Merge branch 'shrinkobl' into trunk	Matthieu Sozeau	2016-06-27
\|\ \
\| * \|	Update CHANGES and COMPATIBILITY	Matthieu Sozeau	2016-06-27
\| * \|	Program: refine shrinking of obligations	Matthieu Sozeau	2016-06-27
\| * \|	Rework treatment of default transparency of obligations	Matthieu Sozeau	2016-06-27
\| * \|	Add Unset Shrink Abstract/Obligations in Coq85	Matthieu Sozeau	2016-06-27
\| * \|	Shrink Proofs/Obligations by default and deprecate	Matthieu Sozeau	2016-06-27
\|/ /
* \|	Typeclasses: fix treatment of exceptions in compat	Matthieu Sozeau	2016-06-27
* \|	Typeclasses: mark unresolvable goals in new implementation	Matthieu Sozeau	2016-06-27
* \|	Fix off-by-1 bug in coq_makefile	Matthieu Sozeau	2016-06-27
* \|	We want tclORELSE to catch exceptions on backtrackings	Matthieu Sozeau	2016-06-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\ \
* \ \	Merge remote-tracking branch 'github/pr/223' into feedback-locations	Maxime Dénès	2016-06-27
\|\ \ \
* \| \| \|	ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTEND	Pierre Letouzey	2016-06-27
* \| \| \|	Merge branch 'sort-fields' into trunk	Maxime Dénès	2016-06-27
\|\ \ \ \
* \ \ \ \	Merge branch 'funpattern-tests' into trunk.	Maxime Dénès	2016-06-27
\|\ \ \ \ \
\| \| * \| \| \|	minor: comment on the meaning of the 'boolean' variable	Gabriel Scherer	2016-06-27
\| \| * \| \| \|	minor: documentation comment for constrintern.ml:sort_fields	Gabriel Scherer	2016-06-27
\| \| * \| \| \|	minor: interp/constrintern.ml, clarify field completion	Gabriel Scherer	2016-06-27
\| \| * \| \| \|	minor: in constrintern.ml:sort_fields, clarify sf	Gabriel Scherer	2016-06-27
\| \| * \| \| \|	add CList.extract_first	Gabriel Scherer	2016-06-27
\| \| * \| \| \|	minor: in constrintern.ml:sort_fields, clarify build_patt	Gabriel Scherer	2016-06-27
\| \| * \| \| \|	whitespace: untabity constrinternl.ml:sort_fields	Gabriel Scherer	2016-06-27
\| \| * \| \| \|	minor clarifications in constrintern.ml:sort_fields	Gabriel Scherer	2016-06-27
\| \|/ / / / \|/\| \| \| \|
\| * \| \| \|	Patterns in binders: printing tests	Arnaud Spiwack	2016-06-27
\| * \| \| \|	Patterns in binders: functional tests	Arnaud Spiwack	2016-06-27
\|/ / / /
* \| \| \|	Merge branch 'funpattern' into trunk. Was PR#142: Binder syntax.	Maxime Dénès	2016-06-27
\|\ \ \ \
\| * \| \| \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27