coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \| \|	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
* \| \|	Typeclasses eauto based on new proof engine,	Matthieu Sozeau	2016-06-16
* \| \|	Refine 9cc95f5, unification of Let-In's, bug #3929	Matthieu Sozeau	2016-06-16
* \| \|	Not taking arguments given by name or position into account when	Hugo Herbelin	2016-06-16
* \| \|	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\ \ \
* \ \ \	Merge branch 'pr/146' into trunk	Enrico Tassi	2016-06-16
\|\ \ \ \
* \| \| \| \|	Fix test-suite for opened bug #4813.	Pierre-Marie Pédrot	2016-06-15
\| * \| \| \|	Merge branch 'pr/146' into trunk	Enrico Tassi	2016-06-15
\|/\| \| \| \|