coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\
\| *	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
* \|	Merge remote-tracking branch 'origin/pr/246' into v8.6	Matthieu Sozeau	2016-08-19
\|\ \
* \| \|	Fixing a collision about the meta-variable ".." in recursive notations.	Hugo Herbelin	2016-07-16
\| * \|	Add test for pi_eq_proofs.	Matthieu Sozeau	2016-07-08
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\ \ \ \| \|/ / \|/\| / \| \|/
* \|	Fixed bug #4622.	Matthieu Sozeau	2016-07-06
* \|	Disallow dependent case on prim records w/o eta	Matthieu Sozeau	2016-07-06
* \|	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
\| \|/
* \|	Adding a test-suite for the only printing flag.	Pierre-Marie Pédrot	2016-06-28
\| *	Forbidding silently dropped universes instances in	Matthieu Sozeau	2016-06-27
* \|	Patterns in binders: functional tests	Arnaud Spiwack	2016-06-27
* \|	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
* \|	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
* \|	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\ \
* \| \|	ssrmatching: simple test for Ltac API	Enrico Tassi	2016-06-15
\| * \|	Ident selectors cannot be used inside an Ltac expression.	Cyprien Mangin	2016-06-14
\| * \|	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
\| * \|	Remove the need for brackets in goal selectors.	Cyprien Mangin	2016-06-14
\| * \|	Add test-suite file for goal selectors.	Cyprien Mangin	2016-06-14
\|/ /
* \|	Improve a comment in the test suite	Jason Gross	2016-06-05
* \|	Make Ltac Profiling an setting	Jason Gross	2016-06-05
* \|	LtacProf for Coq trunk	Jason Gross	2016-06-05
* \|	Update primitive coinductive test-suite.	Matthieu Sozeau	2016-06-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\\|
\| *	An example for cd139311e, showing a consequence of not converting	Hugo Herbelin	2016-04-28
* \|	Fixing a "This clause is redundant" error when interpreting the "in"	Hugo Herbelin	2016-04-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\\|
* \|	Fixing printing of Tactic Notations with tactic arguments.	Pierre-Marie Pédrot	2016-04-08
* \|	An example which failed in 8.5 and that d670c6b6 fixes.	Hugo Herbelin	2016-04-07
\| *	Add -compat 8.4 econstructor tactics, and tests	Jason Gross	2016-04-05
* \|	Fixing an incorrect use of prod_appvect on a term which was not a	Hugo Herbelin	2016-03-28
* \|	Test suite file for a bug in BigQ arithmetic fixed a while ago.	Maxime Dénès	2016-03-25
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-18
\|\\|
\| *	Fix bug when a sort is ascribed to a Record	Matthieu Sozeau	2016-03-15