coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-07-13
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-13
\| \|\
\| \| *	Fixing printing of evar name in an error message of instantiate.	Hugo Herbelin	2016-07-13
* \| \|	A short test on printing evars in Show Proof (this was wrong at some time).	Hugo Herbelin	2016-07-12
\| \| *	Fix test file for #4858.	Maxime Dénès	2016-07-08
\| \| *	Update csdp.cache.	Maxime Dénès	2016-07-08
\| \| *	Test file for #4858.	Maxime Dénès	2016-07-08
\| \| *	Add test file for #4880.	Maxime Dénès	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
\| \|\ \
\| * \| \|	Program: fix #4873: transparency option not used	Matthieu Sozeau	2016-07-07
\| \| \| *	Update csdp.cache.	Maxime Dénès	2016-07-06
\| * \| \|	Fixed bug #4622.	Matthieu Sozeau	2016-07-06
\| * \| \|	Disallow dependent case on prim records w/o eta	Matthieu Sozeau	2016-07-06
\|/ / /
\| \| *	Merge remote-tracking branch 'github/pr/199' into v8.5	Maxime Dénès	2016-07-06
\| \| \|\
\| * \| \|	Fix test-suite file 3690	Matthieu Sozeau	2016-07-06
\|/ / /
\| * \|	congruence fix: test-suite code and update CHANGES	Matthieu Sozeau	2016-07-05
* \| \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
\|\ \ \
\| \| * \|	congruence: Restrict refreshing to Set	Matthieu Sozeau	2016-07-04
\| \| * \|	congruence/univs: properly refresh (fix #4609)	Matthieu Sozeau	2016-07-04
\| \|/ /
\| * \|	test-suite: test checking of libraries checksum.	Maxime Dénès	2016-07-04
* \| \|	Adding test for #4811.	Hugo Herbelin	2016-07-02
\| * \|	Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).	Hugo Herbelin	2016-07-01
* \| \|	Fixing #4865 (deciding on which arguments to recompute scopes was not robust).	Hugo Herbelin	2016-06-29
* \| \|	Univs: Fix bug #4726	Matthieu Sozeau	2016-06-29
* \| \|	Fix issues in test-suite revealed by warnings.	Maxime Dénès	2016-06-29
* \| \|	Adding a test-suite for the only printing flag.	Pierre-Marie Pédrot	2016-06-28
\| * \|	Univs: allowing notations to take univ instances	Matthieu Sozeau	2016-06-27
\| * \|	Forbidding silently dropped universes instances in	Matthieu Sozeau	2016-06-27
* \| \|	Shrink Proofs/Obligations by default and deprecate	Matthieu Sozeau	2016-06-27
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\\| \|
* \| \|	Patterns in binders: printing tests	Arnaud Spiwack	2016-06-27
* \| \|	Patterns in binders: functional tests	Arnaud Spiwack	2016-06-27
* \| \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
\| * \|	More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).	Hugo Herbelin	2016-06-27
* \| \|	Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).	Hugo Herbelin	2016-06-24
* \| \|	Test-suite fix to 1744e37 (injection in context).	Hugo Herbelin	2016-06-18
* \| \|	Adding an "as" clause to specialize.	Hugo Herbelin	2016-06-18
* \| \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \| \|	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
* \| \|	par: like all: but in parallel	Enrico Tassi	2016-06-17
* \| \|	proof mode: print unification constraints	Matthieu Sozeau	2016-06-16
* \| \|	Tentative fix of test-suite file to avoid loop	Matthieu Sozeau	2016-06-16
* \| \|	Cleanup and refactoring	Matthieu Sozeau	2016-06-16
* \| \|	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
* \| \|	Example given at DeepSpec workshop	Matthieu Sozeau	2016-06-16
* \| \|	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
* \| \|	eauto: fix test-suite file	Matthieu Sozeau	2016-06-16
* \| \|	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau	2016-06-16
* \| \|	Fix iterative deepening strategy failing too early	Matthieu Sozeau	2016-06-16