coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	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
* \|	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin	2016-03-13
* \|	Adding a file summarizing the inconsistencies in interpreting implicit	Hugo Herbelin	2016-03-13
\| *	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau	2016-03-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\\|
\| *	Fix strategy of Keyed Unification	Matthieu Sozeau	2016-03-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
* \|	Using build_selector from Equality as a replacement of the selector	Hugo Herbelin	2016-03-05
* \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\| *	Document differences of Hint Resolve and Hint Extern	Matthieu Sozeau	2016-02-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\\|
\| *	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
* \|	Fixing a bug with introduction patterns over inductive types containing let-ins.	Hugo Herbelin	2016-02-18
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|